Newest at the top
| 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) |
| 2025-01-16 15:01:01 +0100 | <hellwolf> | interesting :) |
| 2025-01-16 15:00:59 +0100 | <hellwolf> | "undefined :: GHC.Internal.Stack.Types.HasCallStack => a" |
| 2025-01-16 15:00:28 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 2025-01-16 15:00:27 +0100 | <hellwolf> | > :t undefined |
| 2025-01-16 15:00:21 +0100 | <hellwolf> | :type undefined |
| 2025-01-16 14:58:55 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-01-16 14:58:51 +0100 | akegalj | (~akegalj@89-172-132-1.adsl.net.t-com.hr) (Ping timeout: 244 seconds) |
| 2025-01-16 14:58:46 +0100 | <geekosaur> | "inhabited" |
| 2025-01-16 14:58:40 +0100 | <geekosaur> | try making a value |
| 2025-01-16 14:57:49 +0100 | hellwolf | maybe missing the point here :p |
| 2025-01-16 14:56:46 +0100 | <hellwolf> | does that count? |
| 2025-01-16 14:56:26 +0100 | <hellwolf> | λ newtype A = MkA Void |
| 2025-01-16 14:54:53 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-16 14:52:09 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-16 14:51:49 +0100 | merijn | (~merijn@77.242.116.146) merijn |