2025/03/27

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 +0100ChaiTRex(~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 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2025-03-27 00:01:14 +0100malte(~malte@mal.tc) malte
2025-03-27 00:03:07 +0100merijn(~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 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-03-27 00:09:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-27 00:15:20 +0100dolio(~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in)
2025-03-27 00:20:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 00:20:56 +0100aetepe(~aetepe@188.119.22.83) (Ping timeout: 252 seconds)
2025-03-27 00:21:13 +0100aetepe(~aetepe@46.154.235.16) aetepe
2025-03-27 00:26:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-03-27 00:26:44 +0100dolio(~dolio@130.44.140.168) dolio
2025-03-27 00:27:30 +0100aetepe(~aetepe@46.154.235.16) (Read error: Connection reset by peer)
2025-03-27 00:30:26 +0100dolio(~dolio@130.44.140.168) (Client Quit)
2025-03-27 00:32:04 +0100dolio(~dolio@130.44.140.168) dolio
2025-03-27 00:35:13 +0100lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds)
2025-03-27 00:36:12 +0100Googulator(~Googulato@85-238-67-46.pool.digikabel.hu) (Quit: Client closed)
2025-03-27 00:36:27 +0100Googulator(~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu)
2025-03-27 00:36:39 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 00:39:34 +0100Miroboru(~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 +0100Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru
2025-03-27 00:41:18 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 00:43:30 +0100Googulator(~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu) (Quit: Client closed)
2025-03-27 00:43:43 +0100Googulator(~Googulato@2a01-036d-0106-01d5-c415-995d-99e3-7810.pool6.digikabel.hu)
2025-03-27 00:45:08 +0100malte(~malte@mal.tc) (Ping timeout: 252 seconds)
2025-03-27 00:45:49 +0100aetepe(~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 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 00:57:36 +0100merijn(~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 +0100L29Ah(~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 +0100weary-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 +0100merijn(~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 +0100aetepe(~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 +0100aetepe(~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 +0100jackdkadds `if` to the pile of things that are secretly `id`
2025-03-27 01:13:02 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 01:15:13 +0100sprotte24(~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 +0100yinshrugs
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 +0100Axman6would 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 +0100yin@let if = id
2025-03-27 01:24:00 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 01:24:39 +0100 <Axman6> denied
2025-03-27 01:25:06 +0100Googulator(~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 +0100Googulator(~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 +0100merijn(~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 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-03-27 01:30:30 +0100acidjnk(~acidjnk@p200300d6e71c4f691c99ba8b65f3988d.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2025-03-27 01:30:52 +0100aetepe(~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 +0100peterbecich(~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 +0100emmanuelux(~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 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 01:43:51 +0100malte(~malte@mal.tc) malte
2025-03-27 01:44:53 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection)
2025-03-27 01:45:16 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-03-27 01:45:25 +0100ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-03-27 01:46:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-03-27 01:48:17 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 01:48:26 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-03-27 01:48:26 +0100ljdarj1ljdarj
2025-03-27 01:53:07 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 02:04:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 02:07:54 +0100xff0x(~xff0x@2405:6580:b080:900:d2df:bcfa:d5c3:4ebd) (Ping timeout: 268 seconds)
2025-03-27 02:09:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 02:12:01 +0100werneta(~werneta@syn-071-083-160-242.res.spectrum.com) werneta
2025-03-27 02:14:32 +0100otto_s(~user@p4ff27de5.dip0.t-ipconnect.de) (Ping timeout: 265 seconds)
2025-03-27 02:16:14 +0100otto_s(~user@p5de2f7cc.dip0.t-ipconnect.de)
2025-03-27 02:19:49 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 02:24:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-27 02:32:16 +0100califax(~califax@user/califx) (Remote host closed the connection)
2025-03-27 02:33:24 +0100califax(~califax@user/califx) califx
2025-03-27 02:33:51 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-03-27 02:35:38 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 02:40:21 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 02:41:44 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-03-27 02:47:24 +0100ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)
2025-03-27 02:51:25 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 02:55:45 +0100weary-traveler(~user@user/user363627) user363627
2025-03-27 02:56:24 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 03:03:03 +0100hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds)
2025-03-27 03:07:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 03:12:03 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-27 03:17:09 +0100notdabs(~Owner@2600:1700:69cf:9000:586:19c0:87cb:b0ff) (Read error: Connection reset by peer)
2025-03-27 03:22:42 +0100weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-03-27 03:22:59 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 03:22:59 +0100weary-traveler(~user@user/user363627) user363627
2025-03-27 03:28:54 +0100kaskal-(~kaskal@2a02:8388:15bf:c200:a121:d904:3721:b9c6) (Ping timeout: 260 seconds)
2025-03-27 03:29:33 +0100Ranhir(~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/)
2025-03-27 03:29:38 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-03-27 03:29:39 +0100kaskal(~kaskal@84-115-231-2.cable.dynamic.surfer.at) kaskal
2025-03-27 03:29:45 +0100aetepe(~aetepe@188.119.58.34) aetepe
2025-03-27 03:30:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-27 03:32:06 +0100Ranhir(~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 +0100aetepe(~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 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 244 seconds)
2025-03-27 03:41:03 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 03:45:54 +0100merijn(~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 +0100xff0x(~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 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds)
2025-03-27 03:56:52 +0100merijn(~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 +0100xff0x(~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 +0100merijn(~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 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 04:17:54 +0100merijn(~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 +0100merijn(~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 +0100merijn(~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 +0100merijn(~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 +0100jmcantrell(~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 +0100merijn(~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)