Newest at the top
| 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. |
| 2025-03-27 03:32:06 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
| 2025-03-27 03:30:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-03-27 03:29:45 +0100 | aetepe | (~aetepe@188.119.58.34) aetepe |
| 2025-03-27 03:29:39 +0100 | kaskal | (~kaskal@84-115-231-2.cable.dynamic.surfer.at) kaskal |
| 2025-03-27 03:29:38 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-03-27 03:29:33 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 2025-03-27 03:28:54 +0100 | kaskal- | (~kaskal@2a02:8388:15bf:c200:a121:d904:3721:b9c6) (Ping timeout: 260 seconds) |
| 2025-03-27 03:22:59 +0100 | weary-traveler | (~user@user/user363627) user363627 |