Newest at the top
| 2025-01-16 17:24:11 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:463b:107b:324c:e3d3) ubert |
| 2025-01-16 17:22:45 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-01-16 17:21:45 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-16 17:10:43 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-16 17:08:05 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-01-16 17:04:35 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-16 17:03:58 +0100 | euleritian | (~euleritia@dynamic-176-006-134-022.176.6.pool.telefonica.de) |
| 2025-01-16 17:02:57 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-01-16 17:02:46 +0100 | <haskellbridge> | <Bowuigi> Parametricity gains extra conditions, the evaluation strategy now matters so you gotta be careful when doing equational reasoning, empty types are no longer empty, etc |
| 2025-01-16 17:02:02 +0100 | <haskellbridge> | <Bowuigi> Being able to typecheck a bottom is not a formally nice property because you have one more inhabitant on every type and you have to adapt everything to that |
| 2025-01-16 16:59:55 +0100 | <haskellbridge> | <Bowuigi> Bottom just means "this doesn't work", evaluating one either results in a crash or in infinite recursion |
| 2025-01-16 16:57:23 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-01-16 16:55:18 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-16 16:54:02 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 16:53:43 +0100 | euleritian | (~euleritia@dynamic-176-006-134-022.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-16 16:47:04 +0100 | tnt2 | tnt1 |
| 2025-01-16 16:47:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 245 seconds) |
| 2025-01-16 16:47:00 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
| 2025-01-16 16:46:38 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-16 16:44:05 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-16 16:43:13 +0100 | acidjnk | (~acidjnk@p200300d6e7283f2464fbbfe361ec58f6.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-01-16 16:40:55 +0100 | crvs | (~crvs@185.147.238.3) (Quit: Leaving) |
| 2025-01-16 16:34:19 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-16 16:29:23 +0100 | <EvanR> | the program type checked, bottom is a semantic value |
| 2025-01-16 16:29:04 +0100 | <__monty__> | That's a bottom, and hence an inhabitant, because it type checks. |
| 2025-01-16 16:28:50 +0100 | <EvanR> | you are checking types not values |
| 2025-01-16 16:28:43 +0100 | <EvanR> | exactly |
| 2025-01-16 16:28:26 +0100 | <__monty__> | I have no idea what you mean. You can typecheck an infinite recursion just fine. |
| 2025-01-16 16:28:25 +0100 | <EvanR> | but the heart of abstraction is ignoring stuff |
| 2025-01-16 16:28:08 +0100 | hueso | (~root@user/hueso) hueso |
| 2025-01-16 16:28:00 +0100 | <EvanR> | ignoring shenanigans with undecidable instances |
| 2025-01-16 16:27:44 +0100 | <EvanR> | so if this is just type checking, it still doesn't count |
| 2025-01-16 16:27:27 +0100 | <EvanR> | bottom doesn't exist at type checking time |
| 2025-01-16 16:25:21 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2025-01-16 16:24:19 +0100 | <int-e> | but this is what (some) academics do for fun |
| 2025-01-16 16:23:55 +0100 | <int-e> | (not actually a joke... except that the term is terribly loaded) |
| 2025-01-16 16:22:28 +0100 | <int-e> | Programs don't actually use bottoms very much, so some people argue that they have a moral right to reason about programs as if there were none :P |
| 2025-01-16 16:21:38 +0100 | hueso | (~root@user/hueso) (Ping timeout: 245 seconds) |
| 2025-01-16 16:20:57 +0100 | <geekosaur> | I think the context here is formal reasoning? and bottoms complicate that enormously |
| 2025-01-16 16:19:17 +0100 | <__monty__> | I don't understand the problem, bottom is an inhabitant. You can't actually do anything with it but that doesn't matter, this is type checking, not program execution. |
| 2025-01-16 16:16:58 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3505-d15c-f15c-6f5a-a985-dbfb.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-16 16:15:00 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-16 16:14:07 +0100 | <geekosaur> | bottoms break everything 🙂 |
| 2025-01-16 16:13:26 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3505-d15c-f15c-6f5a-a985-dbfb.rev.sfr.net) alexherbo2 |
| 2025-01-16 16:13:25 +0100 | akegalj | (~akegalj@168-159.dsl.iskon.hr) |
| 2025-01-16 16:12:42 +0100 | <int-e> | So Haskell is morally wrong, then... |
| 2025-01-16 16:12:23 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3505-d15c-e885-791c-fa20-9243.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-16 16:11:34 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-01-16 16:09:35 +0100 | <EvanR> | also this stretches the letter and spirit of inhabited by some |
| 2025-01-16 16:09:13 +0100 | <EvanR> | it's not morally inhabited |