2025/03/27

Newest at the top

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.
2025-03-27 04:04:54 +0100 <monochrom> No, it's too long even for homework.
2025-03-27 04:04:14 +0100 <haskellbridge> <Liamzee> curious, monochrom, have you ever tossed flip flip flip flip into your problem sets?
2025-03-27 04:01:37 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-27 04:00:11 +0100 <monochrom> I guess s/one more dependency/moar dependencies/
2025-03-27 03:59:55 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-03-27 03:59:30 +0100 <monochrom> No, there is no other way.
2025-03-27 03:58:52 +0100 <monochrom> Yes, you add one more dependency.
2025-03-27 03:56:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 03:55:21 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds)
2025-03-27 03:50:55 +0100 <haskellbridge> <Liamzee> (flip flip) flip, not flip (flip flip)
2025-03-27 03:50:37 +0100 <haskellbridge> <Liamzee> ah, i understand
2025-03-27 03:50:19 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-03-27 03:50:07 +0100 <haskellbridge> <Liamzee> flip flip flip?
2025-03-27 03:50:03 +0100 <haskellbridge> <Liamzee> (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2
2025-03-27 03:50:02 +0100 <haskellbridge> <Liamzee> this is weird
2025-03-27 03:45:54 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 03:41:03 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 03:40:04 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 244 seconds)
2025-03-27 03:39:37 +0100 <haskellbridge> <Liamzee> let's see
2025-03-27 03:38:33 +0100 <haskellbridge> <Liamzee> is there a way to use the libraries one of your libraries depend on?
2025-03-27 03:34:44 +0100aetepe(~aetepe@188.119.58.34) (Ping timeout: 260 seconds)
2025-03-27 03:34:43 +0100 <monochrom> If you replace algebraic data types by encoding, you will need RankNTypes. Furthermore, if you pass a value of such a type to a polymorphic function, so for example you pass x :: forall r. r -> (Int -> r) -> r to id :: forall a. a -> a, you also need Impredicativity.