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 +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. |
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 +0100 | merijn | (~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 +0100 | xff0x | (~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 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:55:21 +0100 | xff0x | (~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 +0100 | xff0x | (~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 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 03:41:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:40:04 +0100 | xff0x | (~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 +0100 | aetepe | (~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. |