2025/03/27

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 +0100merijn(~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 +0100jmcantrell(~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 +0100merijn(~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 +0100merijn(~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 +0100merijn(~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 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-27 04:12:37 +0100merijn(~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.