Newest at the top
| 2025-11-21 13:00:58 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 256 seconds) |
| 2025-11-21 12:54:41 +0100 | down200 | (~down200@shell.lug.mtu.edu) down200 |
| 2025-11-21 12:50:02 +0100 | califax | (~califax@user/califx) califx |
| 2025-11-21 12:49:52 +0100 | bwe70296 | (~bwe@2a01:4f8:1c1c:4878::2) bwe |
| 2025-11-21 12:49:41 +0100 | bwe | (~bwe@2a01:4f8:1c1c:4878::2) (Read error: Connection reset by peer) |
| 2025-11-21 12:49:38 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-11-21 12:47:23 +0100 | tromp | (~textual@2001:1c00:3487:1b00:697a:bc7a:f580:408c) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-11-21 12:43:48 +0100 | biberu | (~biberu@user/biberu) biberu |
| 2025-11-21 12:37:57 +0100 | jle` | (~jle`@2603:8001:3b00:11:2f12:c034:12fc:8093) jle` |
| 2025-11-21 12:36:22 +0100 | jle` | (~jle`@2603:8001:3b00:11:658b:1126:1485:2a54) (Ping timeout: 246 seconds) |
| 2025-11-21 12:25:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-21 12:15:50 +0100 | <c_wraith> | But that's what it's going for. |
| 2025-11-21 12:15:32 +0100 | <c_wraith> | It's much more precise than that. |
| 2025-11-21 12:15:24 +0100 | <c_wraith> | domain theory is... sort of adding infinite loops to functions, by introducing a bottom value to represent "this never completes" |
| 2025-11-21 12:14:25 +0100 | <lucabtz> | but thx for the insights, very interesting |
| 2025-11-21 12:13:50 +0100 | <lucabtz> | but you stil lost me with domain theory because i have no idea what it is |
| 2025-11-21 12:12:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-11-21 12:12:44 +0100 | <lucabtz> | c_wraith right |
| 2025-11-21 12:12:26 +0100 | califax | (~califax@user/califx) califx |
| 2025-11-21 12:12:17 +0100 | trickard_ | trickard |
| 2025-11-21 12:11:58 +0100 | <__monty__> | Is Void -> Void a problem for set theory? I can see how a "function" from a non-empty set to Void might be problematic. OTOH can't you say empty sets are not a thing because they're all inhabited by bottom? |
| 2025-11-21 12:11:57 +0100 | <c_wraith> | If you strip out the newtype wrappers, that type is like (((... -> b) -> a) -> b), with infinite recursion on right sides of the arrows. |
| 2025-11-21 12:10:27 +0100 | <lucabtz> | you lost me |
| 2025-11-21 12:09:59 +0100 | Vajb | (~Vajb@n4bl3ovzcj023yptes7-1.v6.elisa-mobile.fi) |
| 2025-11-21 12:09:32 +0100 | <c_wraith> | (you can use hyperfunctions to implement deforestation for zip, for instance) |
| 2025-11-21 12:09:19 +0100 | Vajb | (~Vajb@n6jd7kwb4e2quheg6tf-1.v6.elisa-mobile.fi) (Ping timeout: 264 seconds) |
| 2025-11-21 12:08:24 +0100 | <c_wraith> | but it turns out to actually work in Haskell |
| 2025-11-21 12:08:14 +0100 | <c_wraith> | err, set theory |
| 2025-11-21 12:08:11 +0100 | <c_wraith> | which would be nonsensical in type theory |
| 2025-11-21 12:07:58 +0100 | <c_wraith> | So you get fun things like newtype Hyper a b = H { runH :: Hyper b a -> b } |
| 2025-11-21 12:07:30 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-11-21 12:05:37 +0100 | <probie> | If you don't have an "at least as defined as" operator, are you really living? |
| 2025-11-21 12:05:25 +0100 | <lucabtz> | c_wraith i see, i know nothing about domain theory though |
| 2025-11-21 12:05:17 +0100 | <yin> | imo |
| 2025-11-21 12:05:10 +0100 | <yin> | which is a mistake |
| 2025-11-21 12:04:53 +0100 | <c_wraith> | Haskell is better modeled by domain theory than set theory, as it has explicit bottom values |
| 2025-11-21 12:04:10 +0100 | <lucabtz> | chromoblob yep |
| 2025-11-21 12:04:04 +0100 | califax | (~califax@user/califx) (Ping timeout: 272 seconds) |
| 2025-11-21 12:03:41 +0100 | EvanR | (~EvanR@user/evanr) (Ping timeout: 264 seconds) |
| 2025-11-21 12:03:34 +0100 | <yin> | does the Yoneda Lemma apply? |
| 2025-11-21 12:03:30 +0100 | <lucabtz> | but does not exclude {} in the example A = B = {} |
| 2025-11-21 12:03:28 +0100 | <chromoblob> | yeah, i wanted to lead to this |
| 2025-11-21 12:03:14 +0100 | <lucabtz> | which does exclude {} from the example of A = B = {1} |
| 2025-11-21 12:03:03 +0100 | mesaoptimizer | (~user@user/PapuaHardyNet) PapuaHardyNet |
| 2025-11-21 12:03:02 +0100 | <c_wraith> | lucabtz: in set theory, yes. In domain theory? |
| 2025-11-21 12:02:52 +0100 | <lambdabot> | Void -> Void |
| 2025-11-21 12:02:51 +0100 | <[exa]> | :t id :: Void -> Void |
| 2025-11-21 12:02:48 +0100 | <lucabtz> | chromoblob i think in general a subset of A x B is called a relation between A and B. for a function the relation has to assign a single element of B to each and every element of A |
| 2025-11-21 12:02:44 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) fp |
| 2025-11-21 12:02:36 +0100 | <haskellbridge> | <Morj> chromoblob: How extentional of you |