Newest at the top
| 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 |
| 2025-11-21 12:02:01 +0100 | <c_wraith> | because there are multiple concepts of function, and a lot of the disagreement is coming from set theory vs domain theory |
| 2025-11-21 12:01:54 +0100 | <chromoblob> | Morj: one, because any two are indistinguishable |
| 2025-11-21 12:01:32 +0100 | <c_wraith> | here's where things get annoying: you need to be more precise than "function" |
| 2025-11-21 12:01:26 +0100 | <chromoblob> | lucabtz: which restrictions are there on the subset? |
| 2025-11-21 12:01:25 +0100 | <haskellbridge> | <Morj> But how many functions are there from bottom to bottom? One or infinitely many? |
| 2025-11-21 12:01:12 +0100 | EvanR_ | (~EvanR@user/evanr) EvanR |
| 2025-11-21 12:01:01 +0100 | <yin> | and how many functions are there of the type Void -> Void? |
| 2025-11-21 12:00:32 +0100 | <chromoblob> | yin: yes, () would correspond to 1 |
| 2025-11-21 12:00:27 +0100 | <c_wraith> | yes |
| 2025-11-21 12:00:25 +0100 | <lucabtz> | since A x B = {(1, 1)} you have both {} and {(1, 1)} |
| 2025-11-21 12:00:15 +0100 | <yin> | 0^0 would be Void -> Void and not () -> () right? |