Newest at the top
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 |
2025-03-27 04:41:25 +0100 | <haskellbridge> | <Liamzee> i was really asking about whether the only non-trivial value is (\u@(Mu a) -> a u), which is still a bottom |
2025-03-27 04:40:49 +0100 | <haskellbridge> | <Liamzee> forall a |
2025-03-27 04:40:43 +0100 | <EvanR> | squint |
2025-03-27 04:40:23 +0100 | <haskellbridge> | <Liamzee> forall Mu a... cardinality is 0 if you consider the bottom triggered by non-termination not to count |
2025-03-27 04:39:33 +0100 | <EvanR> | (but not others) |
2025-03-27 04:39:26 +0100 | <EvanR> | (in hott, some types are (h-)sets) |
2025-03-27 04:39:19 +0100 | <haskellbridge> | <Liamzee> blame Sandy Maguire's thinking with types |
2025-03-27 04:38:31 +0100 | <EvanR> | types aren't sets so no cardinality at all |
2025-03-27 04:33:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 04:30:49 +0100 | <monochrom> | No. |
2025-03-27 04:28:44 +0100 | <haskellbridge> | <Liamzee> and wait, that type has a cardinality of 1? |
2025-03-27 04:28:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 04:25:32 +0100 | <monochrom> | You need a newtype wrapper because it's a recursive type. Type alias doesn't support recursive alias. |
2025-03-27 04:23:39 +0100 | <haskellbridge> | <Liamzee> thanks, so newtype Mu a = Mu (Mu a -> a), but not type Mu a = (Mu a -> a) |
2025-03-27 04:17:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-03-27 04:12:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 04:07:18 +0100 | <monochrom> | But I give (\x -> x x) so students see occurs check in action. |
2025-03-27 04:06:29 +0100 | <monochrom> | Maybe (.) (.) is reasonably long and short. |
2025-03-27 04:06:15 +0100 | <haskellbridge> | <Liamzee> i still haven't figured out how it unifies |
2025-03-27 04:05:22 +0100 | <monochrom> | Also, I only mean too long for my TAs to mark. |