Newest at the top
| 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 |
| 2025-01-16 16:08:33 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-16 16:08:10 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-01-16 16:04:07 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-16 16:03:44 +0100 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-01-16 16:02:18 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 246 seconds) |
| 2025-01-16 16:00:55 +0100 | ephilalethes | (~noumenon@36.83.232.119) (Quit: Leaving) |
| 2025-01-16 15:58:54 +0100 | <hellwolf> | do you need a visa for it? |
| 2025-01-16 15:56:17 +0100 | CiaoSen | (~Jura@2a05:5800:21a:4900:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2025-01-16 15:53:37 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-16 15:53:01 +0100 | euleritian | (~euleritia@dynamic-176-006-134-022.176.6.pool.telefonica.de) |
| 2025-01-16 15:52:40 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-16 15:52:17 +0100 | housemate | (~housemate@146.70.66.228) (Ping timeout: 252 seconds) |
| 2025-01-16 15:50:17 +0100 | chele | (~chele@user/chele) chele |
| 2025-01-16 15:39:46 +0100 | CiaoSen | (~Jura@2a05:5800:21a:4900:ca4b:d6ff:fec1:99da) CiaoSen |
| 2025-01-16 15:32:57 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2025-01-16 15:32:55 +0100 | <kuribas> | if it's defined as "data Void" |
| 2025-01-16 15:24:27 +0100 | ephilalethes | (~noumenon@36.83.232.119) noumenon |
| 2025-01-16 15:04:34 +0100 | <kuribas> | hellwolf: Void is actually inhabited :-O |
| 2025-01-16 15:04:28 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-16 15:03:40 +0100 | vpan | (~vpan@212.117.1.172) |
| 2025-01-16 15:03:10 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2025-01-16 15:01:45 +0100 | <hellwolf> | undefined = raise# (errorCallWithCallStackException "Prelude.undefined" ?callStack) |