2025-03-27 00:00:05 +0100 | <jle`> | ah then i should probably file a report, i've run into two different ado related bugs recently i think |
2025-03-27 00:00:33 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
2025-03-27 00:00:41 +0100 | <jle`> | one using NamedFieldPuns/RecordWildCards and one with existential types/type abstractions |
2025-03-27 00:00:56 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
2025-03-27 00:01:14 +0100 | malte | (~malte@mal.tc) malte |
2025-03-27 00:03:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 00:03:34 +0100 | <jle`> | i have been getting around it by manually >>=-ing at the points that cause issues |
2025-03-27 00:03:53 +0100 | <jle`> | at the cost of a layer of indentation :') |
2025-03-27 00:05:59 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
2025-03-27 00:09:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-03-27 00:15:20 +0100 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-03-27 00:20:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 00:20:56 +0100 | aetepe | (~aetepe@188.119.22.83) (Ping timeout: 252 seconds) |
2025-03-27 00:21:13 +0100 | aetepe | (~aetepe@46.154.235.16) aetepe |
2025-03-27 00:26:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-03-27 00:26:44 +0100 | dolio | (~dolio@130.44.140.168) dolio |
2025-03-27 00:27:30 +0100 | aetepe | (~aetepe@46.154.235.16) (Read error: Connection reset by peer) |
2025-03-27 00:30:26 +0100 | dolio | (~dolio@130.44.140.168) (Client Quit) |
2025-03-27 00:32:04 +0100 | dolio | (~dolio@130.44.140.168) dolio |
2025-03-27 00:35:13 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
2025-03-27 00:36:12 +0100 | Googulator | (~Googulato@85-238-67-46.pool.digikabel.hu) (Quit: Client closed) |
2025-03-27 00:36:27 +0100 | Googulator | (~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) |
2025-03-27 00:36:39 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 00:39:34 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 260 seconds) |
2025-03-27 00:39:35 +0100 | <yin> | did i dream that we could turn off if ... then ... else syntax? |
2025-03-27 00:40:35 +0100 | <yin> | or was it an april's fool joke? |
2025-03-27 00:40:48 +0100 | <geekosaur> | you dreamed it, I think. maybe you were thinking of RebindableSyntax translating it into a user-supplied ifThenElse function? |
2025-03-27 00:41:02 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru |
2025-03-27 00:41:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-27 00:43:30 +0100 | Googulator | (~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) (Quit: Client closed) |
2025-03-27 00:43:43 +0100 | Googulator | (~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) |
2025-03-27 00:45:08 +0100 | malte | (~malte@mal.tc) (Ping timeout: 252 seconds) |
2025-03-27 00:45:49 +0100 | aetepe | (~aetepe@46.154.235.16) aetepe |
2025-03-27 00:48:45 +0100 | <haskellbridge> | <Bowuigi> I get why one would want to rebind it, but why removing it? yin |
2025-03-27 00:52:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 00:57:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-03-27 00:58:52 +0100 | <yin> | just purism |
2025-03-27 01:00:02 +0100 | <yin> | syntactic sugar allergy |
2025-03-27 01:00:20 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2025-03-27 01:04:21 +0100 | <geekosaur> | you're going to have to delete most of Haskell if you don't like syntactic sugar. even standard Haskell is full of it |
2025-03-27 01:04:39 +0100 | <yin> | True |
2025-03-27 01:05:28 +0100 | <jackdk> | yin: you mean `\a b -> a` |
2025-03-27 01:05:57 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-03-27 01:06:41 +0100 | <yin> | jackdk: const? |
2025-03-27 01:07:14 +0100 | <yin> | or "anonymous lambdas" in general? |
2025-03-27 01:07:18 +0100 | <jackdk> | Desugaring `True` into a Church-encoded boolean, and making the tongue-in-cheek claim that even algebraic data types are syntactic sugar |
2025-03-27 01:07:27 +0100 | <yin> | ah i see |
2025-03-27 01:08:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 01:09:09 +0100 | <jackdk> | At which point you can get rid of `if..then..else` expressions by directly applying the "then" and the "else" directly to your Church boolean and letting it pick which one to return |
2025-03-27 01:09:29 +0100 | aetepe | (~aetepe@46.154.235.16) (Read error: Connection reset by peer) |
2025-03-27 01:09:35 +0100 | <yin> | jackdk: if you go down that route you'll have interesting discussions with the type system when you get into things like the Y combinator |
2025-03-27 01:10:16 +0100 | <geekosaur> | you're going to have interesting discussions with it about the Y combinator anyway 🙂 |
2025-03-27 01:10:20 +0100 | aetepe | (~aetepe@46.154.235.16) aetepe |
2025-03-27 01:11:30 +0100 | <yin> | jackdk: if = id -- ;) |
2025-03-27 01:11:52 +0100 | <yin> | geekosaur: not False |
2025-03-27 01:12:03 +0100 | jackdk | adds `if` to the pile of things that are secretly `id` |
2025-03-27 01:13:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-27 01:15:13 +0100 | sprotte24 | (~sprotte24@p200300d16f097d007520d57df2b917ec.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
2025-03-27 01:16:06 +0100 | <yin> | newtype Mu a = Mu (Mu a -> a) |
2025-03-27 01:16:26 +0100 | <yin> | is this right? |
2025-03-27 01:17:12 +0100 | <yin> | y f = (\x -> f (x (Mu x))) (\(Mu x) -> f (x (Mu x))) |
2025-03-27 01:17:57 +0100 | <yin> | > let y f = (\x -> f (x (Mu x))) (\(Mu x) -> f (x (Mu x))) in take 10 $ y (1:) |
2025-03-27 01:17:58 +0100 | <lambdabot> | error: |
2025-03-27 01:17:58 +0100 | <lambdabot> | Not in scope: data constructor ‘Mu’ |
2025-03-27 01:17:58 +0100 | <lambdabot> | Perhaps you meant one of these: |
2025-03-27 01:18:22 +0100 | <yin> | > newtype Mu a = Mu (Mu a -> a); let y f = (\x -> f (x (Mu x))) (\(Mu x) -> f (x (Mu x))) in take 10 $ y (1:) |
2025-03-27 01:18:23 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘newtype’ |
2025-03-27 01:18:33 +0100 | yin | shrugs |
2025-03-27 01:18:34 +0100 | <geekosaur> | use @let for the newtype |
2025-03-27 01:18:51 +0100 | <geekosaur> | (and for let in general) |
2025-03-27 01:18:56 +0100 | Axman6 | would argue that in Haskell, the proper church encoding of True would be \a b -> b given the order of Bool's constructors |
2025-03-27 01:19:25 +0100 | <yin> | :t bool |
2025-03-27 01:19:26 +0100 | <lambdabot> | a -> a -> Bool -> a |
2025-03-27 01:19:40 +0100 | <Axman6> | > bool "a" "b" True |
2025-03-27 01:19:41 +0100 | <lambdabot> | "b" |
2025-03-27 01:20:16 +0100 | <yin> | geekosaur: can you show me how to do that? |
2025-03-27 01:20:29 +0100 | <Axman6> | @let newtype Mu a = Mu (Mu a -> a) |
2025-03-27 01:20:30 +0100 | <lambdabot> | Defined. |
2025-03-27 01:20:40 +0100 | <Axman6> | > let y f = (\x -> f (x (Mu x))) (\(Mu x) -> f (x (Mu x))) in take 10 $ y (1:) |
2025-03-27 01:20:41 +0100 | <lambdabot> | [1,1,1,1,1,1,1,1,1,1] |
2025-03-27 01:21:14 +0100 | <yin> | nice. didn't know we could pollute lambdabot |
2025-03-27 01:22:24 +0100 | <geekosaur> | "@undefine" clears it |
2025-03-27 01:22:31 +0100 | <geekosaur> | (but it's all or nothing) |
2025-03-27 01:23:48 +0100 | yin | @let if = id |
2025-03-27 01:24:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 01:24:39 +0100 | <Axman6> | denied |
2025-03-27 01:25:06 +0100 | Googulator | (~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) (Quit: Client closed) |
2025-03-27 01:25:15 +0100 | <yin> | i remember one of my first questions in #haskell-beginners being about some mess i got into because i had overloaded (+) in ghci |
2025-03-27 01:25:19 +0100 | <yin> | fun times |
2025-03-27 01:25:20 +0100 | Googulator | (~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) |
2025-03-27 01:27:56 +0100 | <jackdk> | Axman6: what else is on the `id` list? I can think of `($)` and lens's `traversal`, `(%%~)`, `simply`, `simple`, `equality Refl Refl` and `equality' Refl` |
2025-03-27 01:28:19 +0100 | <yin> | i also cherish the first time someone answered me a (simple, i thought) question with a link to a white paper |
2025-03-27 01:28:43 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-03-27 01:29:03 +0100 | <Axman6> | You'd probably find two dozen foo = id in lens |
2025-03-27 01:29:12 +0100 | <Axman6> | how good are types |
2025-03-27 01:29:31 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2025-03-27 01:30:30 +0100 | acidjnk | (~acidjnk@p200300d6e71c4f691c99ba8b65f3988d.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
2025-03-27 01:30:52 +0100 | aetepe | (~aetepe@46.154.235.16) (Read error: Connection reset by peer) |
2025-03-27 01:31:27 +0100 | <yin> | :t flip |
2025-03-27 01:31:28 +0100 | <lambdabot> | (a -> b -> c) -> b -> a -> c |
2025-03-27 01:31:29 +0100 | <yin> | :t flip flip |
2025-03-27 01:31:30 +0100 | <lambdabot> | b -> (a -> b -> c) -> a -> c |
2025-03-27 01:31:34 +0100 | <yin> | :t flip flip flip |
2025-03-27 01:31:35 +0100 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
2025-03-27 01:31:36 +0100 | <yin> | :t flip flip flip flip |
2025-03-27 01:31:37 +0100 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
2025-03-27 01:31:40 +0100 | <yin> | :t flip flip flip flip flip |
2025-03-27 01:31:41 +0100 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
2025-03-27 01:31:45 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-03-27 01:31:53 +0100 | <yin> | one of my favourites |
2025-03-27 01:32:50 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
2025-03-27 01:33:05 +0100 | <yin> | took me half an afternoon to understand this back in the day |
2025-03-27 01:34:50 +0100 | <Axman6> | this one surprises me, I guess I'd need to sit down and figure it out too |
2025-03-27 01:37:16 +0100 | <yin> | the function type always trips me up |
2025-03-27 01:38:46 +0100 | <yin> | type level fixed point |
2025-03-27 01:39:47 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 01:43:51 +0100 | malte | (~malte@mal.tc) malte |
2025-03-27 01:44:53 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
2025-03-27 01:45:16 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
2025-03-27 01:45:25 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-03-27 01:46:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
2025-03-27 01:48:17 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 01:48:26 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-03-27 01:48:26 +0100 | ljdarj1 | ljdarj |
2025-03-27 01:53:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-27 02:04:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 02:07:54 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d2df:bcfa:d5c3:4ebd) (Ping timeout: 268 seconds) |
2025-03-27 02:09:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 02:12:01 +0100 | werneta | (~werneta@syn-071-083-160-242.res.spectrum.com) werneta |
2025-03-27 02:14:32 +0100 | otto_s | (~user@p4ff27de5.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
2025-03-27 02:16:14 +0100 | otto_s | (~user@p5de2f7cc.dip0.t-ipconnect.de) |
2025-03-27 02:19:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 02:24:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-03-27 02:32:16 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2025-03-27 02:33:24 +0100 | califax | (~califax@user/califx) califx |
2025-03-27 02:33:51 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2025-03-27 02:35:38 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 02:40:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-27 02:41:44 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-03-27 02:47:24 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
2025-03-27 02:51:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 02:55:45 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-03-27 02:56:24 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 03:03:03 +0100 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
2025-03-27 03:07:15 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:12:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-03-27 03:17:09 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:586:19c0:87cb:b0ff) (Read error: Connection reset by peer) |
2025-03-27 03:22:42 +0100 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
2025-03-27 03:22:59 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:22:59 +0100 | weary-traveler | (~user@user/user363627) user363627 |
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:29:33 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
2025-03-27 03:29:38 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
2025-03-27 03:29:39 +0100 | kaskal | (~kaskal@84-115-231-2.cable.dynamic.surfer.at) kaskal |
2025-03-27 03:29:45 +0100 | aetepe | (~aetepe@188.119.58.34) aetepe |
2025-03-27 03:30:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-03-27 03:32:06 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
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:34:44 +0100 | aetepe | (~aetepe@188.119.58.34) (Ping timeout: 260 seconds) |
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:39:37 +0100 | <haskellbridge> | <Liamzee> let's see |
2025-03-27 03:40:04 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 244 seconds) |
2025-03-27 03:41:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:45:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 03:50:02 +0100 | <haskellbridge> | <Liamzee> this is weird |
2025-03-27 03:50:03 +0100 | <haskellbridge> | <Liamzee> (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
2025-03-27 03:50:07 +0100 | <haskellbridge> | <Liamzee> flip flip flip? |
2025-03-27 03:50:19 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
2025-03-27 03:50:37 +0100 | <haskellbridge> | <Liamzee> ah, i understand |
2025-03-27 03:50:55 +0100 | <haskellbridge> | <Liamzee> (flip flip) flip, not flip (flip flip) |
2025-03-27 03:55:21 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
2025-03-27 03:56:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 03:58:52 +0100 | <monochrom> | Yes, you add one more dependency. |
2025-03-27 03:59:30 +0100 | <monochrom> | No, there is no other way. |
2025-03-27 03:59:55 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
2025-03-27 04:00:11 +0100 | <monochrom> | I guess s/one more dependency/moar dependencies/ |
2025-03-27 04:01:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
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:04:54 +0100 | <monochrom> | No, it's too long even for homework. |
2025-03-27 04:05:22 +0100 | <monochrom> | Also, I only mean too long for my TAs to mark. |
2025-03-27 04:06:15 +0100 | <haskellbridge> | <Liamzee> i still haven't figured out how it unifies |
2025-03-27 04:06:29 +0100 | <monochrom> | Maybe (.) (.) is reasonably long and short. |
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:12:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 04:17:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
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: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:28:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-27 04:28:44 +0100 | <haskellbridge> | <Liamzee> and wait, that type has a cardinality of 1? |
2025-03-27 04:30:49 +0100 | <monochrom> | No. |
2025-03-27 04:33:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-03-27 04:38:31 +0100 | <EvanR> | types aren't sets so no cardinality at all |
2025-03-27 04:39:19 +0100 | <haskellbridge> | <Liamzee> blame Sandy Maguire's thinking with types |
2025-03-27 04:39:26 +0100 | <EvanR> | (in hott, some types are (h-)sets) |
2025-03-27 04:39:33 +0100 | <EvanR> | (but not others) |
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:40:43 +0100 | <EvanR> | squint |
2025-03-27 04:40:49 +0100 | <haskellbridge> | <Liamzee> forall a |
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:41:45 +0100 | <EvanR> | a lambda is not a bottom |
2025-03-27 04:42:24 +0100 | <haskellbridge> | <Liamzee> okay, it's not a bottom |
2025-03-27 04:42:39 +0100 | <haskellbridge> | <Liamzee> but is this the only implementable lambda? |
2025-03-27 04:42:50 +0100 | <EvanR> | what is the type of that lambdas body |
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:43:05 +0100 | <haskellbridge> | <Liamzee> (Mu a -> a) |
2025-03-27 04:43:20 +0100 | <EvanR> | to construct a lambda... |
2025-03-27 04:43:22 +0100 | <EvanR> | oops |
2025-03-27 04:43:24 +0100 | <EvanR> | gave it away |
2025-03-27 04:43:42 +0100 | <EvanR> | to construct a inhabitant of function type... |
2025-03-27 04:44:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
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: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:46:19 +0100 | <EvanR> | I think you can explicitly show at least 2 |
2025-03-27 04:46:27 +0100 | <EvanR> | the one above is explicitly 1 |
2025-03-27 04:46:28 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
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:47:24 +0100 | <EvanR> | yes I'm not sure if quantifying makes it easier or harder |
2025-03-27 04:48:45 +0100 | <monochrom> | Oh, parametricity always collapses the space. But that's a disgression. |
2025-03-27 04:49:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
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:50:28 +0100 | <EvanR> | kind of like if you need a Nat, you can always say Z |
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:51:55 +0100 | <EvanR> | id . id is different from id as terms, but are equal by function extensionality |
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) |