Newest at the top
2025-03-27 05:06:25 +0100 | <haskellbridge> | <Bowuigi> They are equal under function extensionality |
2025-03-27 05:06:22 +0100 | <haskellbridge> | <Liamzee> ah |
2025-03-27 05:06:13 +0100 | <haskellbridge> | <Liamzee> also (\x -> bottom) can be evaluated without triggering bottom? |
2025-03-27 05:06:11 +0100 | <EvanR> | but you might be right there's no way to observe the difference |
2025-03-27 05:06:09 +0100 | <monochrom> | I know Haskell's seq can distinguish them. But I also know that the Haskell Report confesses that this is why seq deviates from denotational semantics. |
2025-03-27 05:05:14 +0100 | <EvanR> | one is more defined than the other, obviously |
2025-03-27 05:05:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 05:04:59 +0100 | <monochrom> | I have trouble distinguishing ⊥ from \x -> ⊥ |
2025-03-27 05:04:15 +0100 | <haskellbridge> | <Bowuigi> Yes |
2025-03-27 05:03:57 +0100 | <EvanR> | ⊥, \x -> x, \x -> ⊥, \x -> () |
2025-03-27 05:03:56 +0100 | <haskellbridge> | <Bowuigi> Backslashes* |
2025-03-27 05:03:37 +0100 | <haskellbridge> | <Bowuigi> Matrix might have eaten some parens |
2025-03-27 05:03:22 +0100 | <haskellbridge> | <Bowuigi> Sorry, \x -> bottom and \() -> bottom |
2025-03-27 05:02:50 +0100 | <haskellbridge> | <Bowuigi> \x -> bottom and _ -> bottom are the same thing, () -> bottom is \x -> case x of () -> bottom which already returns bottom on every case |
2025-03-27 05:02:13 +0100 | <monochrom> | Oh you can always proofread and edit before pressing enter. |
2025-03-27 05:01:46 +0100 | <haskellbridge> | <Liamzee> i wish i could delete my imprecise blather |
2025-03-27 05:01:38 +0100 | <EvanR> | at the very least, use a universe |
2025-03-27 05:01:17 +0100 | <EvanR> | "the cardinality of all types" wwwwwwwwhwhhhhhaaaaaaaat |
2025-03-27 05:01:00 +0100 | <haskellbridge> | <Liamzee> i mean if you restrict a, instead of newtyping, it's equal to the cardinality of all types |
2025-03-27 05:00:57 +0100 | <haskellbridge> | <Bowuigi> Yeah |
2025-03-27 05:00:54 +0100 | <haskellbridge> | <Bowuigi> \x -> () |
2025-03-27 05:00:43 +0100 | <EvanR> | \x -> () |
2025-03-27 05:00:35 +0100 | <EvanR> | ? |
2025-03-27 05:00:33 +0100 | <EvanR> | \() -> ⊥ |
2025-03-27 05:00:05 +0100 | <EvanR> | ⊥, \x -> x, \x -> ⊥, |
2025-03-27 05:00:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 04:59:16 +0100 | <EvanR> | for () -> () you'd have |
2025-03-27 04:58:53 +0100 | <EvanR> | if you use domains, for Nat you'd have ⊥, Z, S ⊥, S Z, S (S ⊥), S (S Z), ... |
2025-03-27 04:56:53 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-03-27 04:56:44 +0100 | <haskellbridge> | <Liamzee> so in that case, the only inhabitant is a value that produces bottom, which i guess is 1 |
2025-03-27 04:56:22 +0100 | <haskellbridge> | <Liamzee> sorry, my mistake for not being specific |
2025-03-27 04:56:10 +0100 | <EvanR> | newtype Mu a = Mu (Mu a -> a) |
2025-03-27 04:54:01 +0100 | <EvanR> | where exactly, since I asked what the type needed to be and you said "function" |
2025-03-27 04:53:46 +0100 | <haskellbridge> | <Liamzee> yes, but how would you manufacture a non-bottom value of type a? |
2025-03-27 04:53:31 +0100 | <haskellbridge> | <Liamzee> or rather the typechecker |
2025-03-27 04:53:30 +0100 | <EvanR> | you could have used a non-bottom value in the body of your function earlier |
2025-03-27 04:52:57 +0100 | <EvanR> | Mu a is a type and bottom is a value... so Mu a -> bottom is causing the computer to self destruct now |
2025-03-27 04:52:14 +0100 | <haskellbridge> | <Liamzee> but for all intents and purposes, i guess, (Mu a -> a) given parametricity has either 0 or 1 inhabitants, because it's always (Mu a -> bottom) |
2025-03-27 04:51:55 +0100 | <EvanR> | id . id is different from id as terms, but are equal by function extensionality |
2025-03-27 04:51:08 +0100 | <haskellbridge> | <Liamzee> it feels like pretending id.id is distinct from id and then claiming that a -> a has multiple inhabitants |
2025-03-27 04:50:28 +0100 | <EvanR> | kind of like if you need a Nat, you can always say Z |
2025-03-27 04:49:11 +0100 | <EvanR> | Liamzee, if in someplace you need something of function type, and you don't have any other options, you can always say "lambda such and such" |
2025-03-27 04:49:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-03-27 04:48:45 +0100 | <monochrom> | Oh, parametricity always collapses the space. But that's a disgression. |
2025-03-27 04:47:24 +0100 | <EvanR> | yes I'm not sure if quantifying makes it easier or harder |
2025-03-27 04:47:05 +0100 | <monochrom> | Mu Int has more than Int, namely, Mu (const i) for each i :: Int. |
2025-03-27 04:46:28 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
2025-03-27 04:46:27 +0100 | <EvanR> | the one above is explicitly 1 |
2025-03-27 04:46:19 +0100 | <EvanR> | I think you can explicitly show at least 2 |
2025-03-27 04:45:35 +0100 | <haskellbridge> | <Liamzee> so implicitly, there is another function that exists in the type (forall a. Mu a -> a), |