Newest at the top
| 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), |
| 2025-03-27 04:44:55 +0100 | <EvanR> | the domains tend to have a lot more that you'd expect from a naive set interpretation |
| 2025-03-27 04:44:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-27 04:43:42 +0100 | <EvanR> | to construct a inhabitant of function type... |
| 2025-03-27 04:43:24 +0100 | <EvanR> | gave it away |
| 2025-03-27 04:43:22 +0100 | <EvanR> | oops |
| 2025-03-27 04:43:20 +0100 | <EvanR> | to construct a lambda... |
| 2025-03-27 04:43:05 +0100 | <haskellbridge> | <Liamzee> (Mu a -> a) |
| 2025-03-27 04:42:54 +0100 | <monochrom> | Since recursion is involved, you should use denotational domains (rather than any type theory) for types. A denotational domain is a partially ordered set, but you can forget the partial order part and ask about the cardinality of the set part. The cardinality for the set for Mu is going to be infinite. |
| 2025-03-27 04:42:50 +0100 | <EvanR> | what is the type of that lambdas body |
| 2025-03-27 04:42:39 +0100 | <haskellbridge> | <Liamzee> but is this the only implementable lambda? |
| 2025-03-27 04:42:24 +0100 | <haskellbridge> | <Liamzee> okay, it's not a bottom |
| 2025-03-27 04:41:45 +0100 | <EvanR> | a lambda is not a bottom |