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)
2025-03-27 04:52:57 +0100 <EvanR> Mu a is a type and bottom is a value... so Mu a -> bottom is causing the computer to self destruct now
2025-03-27 04:53:30 +0100 <EvanR> you could have used a non-bottom value in the body of your function earlier
2025-03-27 04:53:31 +0100 <haskellbridge> <Liamzee> or rather the typechecker
2025-03-27 04:53:46 +0100 <haskellbridge> <Liamzee> yes, but how would you manufacture a non-bottom value of type a?
2025-03-27 04:54:01 +0100 <EvanR> where exactly, since I asked what the type needed to be and you said "function"
2025-03-27 04:56:10 +0100 <EvanR> newtype Mu a = Mu (Mu a -> a)
2025-03-27 04:56:22 +0100 <haskellbridge> <Liamzee> sorry, my mistake for not being specific
2025-03-27 04:56:44 +0100 <haskellbridge> <Liamzee> so in that case, the only inhabitant is a value that produces bottom, which i guess is 1
2025-03-27 04:56:53 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-03-27 04:58:53 +0100 <EvanR> if you use domains, for Nat you'd have ⊥, Z, S ⊥, S Z, S (S ⊥), S (S Z), ...
2025-03-27 04:59:16 +0100 <EvanR> for () -> () you'd have
2025-03-27 05:00:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 05:00:05 +0100 <EvanR> ⊥, \x -> x, \x -> ⊥,
2025-03-27 05:00:33 +0100 <EvanR> \() -> ⊥
2025-03-27 05:00:35 +0100 <EvanR> ?
2025-03-27 05:00:43 +0100 <EvanR> \x -> ()
2025-03-27 05:00:54 +0100 <haskellbridge> <Bowuigi> \x -> ()
2025-03-27 05:00:57 +0100 <haskellbridge> <Bowuigi> Yeah
2025-03-27 05:01:00 +0100 <haskellbridge> <Liamzee> i mean if you restrict a, instead of newtyping, it's equal to the cardinality of all types
2025-03-27 05:01:17 +0100 <EvanR> "the cardinality of all types" wwwwwwwwhwhhhhhaaaaaaaat
2025-03-27 05:01:38 +0100 <EvanR> at the very least, use a universe
2025-03-27 05:01:46 +0100 <haskellbridge> <Liamzee> i wish i could delete my imprecise blather
2025-03-27 05:02:13 +0100 <monochrom> Oh you can always proofread and edit before pressing enter.
2025-03-27 05:02:50 +0100 <haskellbridge> <Bowuigi> \x -> bottom and _ -> bottom are the same thing, () -> bottom is \x -> case x of () -> bottom which already returns bottom on every case
2025-03-27 05:03:22 +0100 <haskellbridge> <Bowuigi> Sorry, \x -> bottom and \() -> bottom
2025-03-27 05:03:37 +0100 <haskellbridge> <Bowuigi> Matrix might have eaten some parens
2025-03-27 05:03:56 +0100 <haskellbridge> <Bowuigi> Backslashes*
2025-03-27 05:03:57 +0100 <EvanR> ⊥, \x -> x, \x -> ⊥, \x -> ()
2025-03-27 05:04:15 +0100 <haskellbridge> <Bowuigi> Yes
2025-03-27 05:04:59 +0100 <monochrom> I have trouble distinguishing ⊥ from \x -> ⊥
2025-03-27 05:05:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 05:05:14 +0100 <EvanR> one is more defined than the other, obviously
2025-03-27 05:06:09 +0100 <monochrom> I know Haskell's seq can distinguish them. But I also know that the Haskell Report confesses that this is why seq deviates from denotational semantics.
2025-03-27 05:06:11 +0100 <EvanR> but you might be right there's no way to observe the difference
2025-03-27 05:06:13 +0100 <haskellbridge> <Liamzee> also (\x -> bottom) can be evaluated without triggering bottom?
2025-03-27 05:06:22 +0100 <haskellbridge> <Liamzee> ah
2025-03-27 05:06:25 +0100 <haskellbridge> <Bowuigi> They are equal under function extensionality
2025-03-27 05:06:57 +0100 <haskellbridge> <Bowuigi> (Assuming the usual 'bottom x = bottom')
2025-03-27 05:07:23 +0100 <EvanR> so maybe domains didn't help clear up "how to count" as much as you hoped
2025-03-27 05:08:24 +0100 <haskellbridge> <Bowuigi> Assuming totality and equating using funext/homotopies is an easy way to get most of the useful terms
2025-03-27 05:08:46 +0100 <monochrom> Oh domains are difficult, it never "helps" to get them involved. But I was going for clarifying *what* to count.
2025-03-27 05:09:03 +0100 <EvanR> assuming totality, that seems to call for a whole different semantics
2025-03-27 05:09:10 +0100 <haskellbridge> <Bowuigi> But in this case you wanted to get the members of a fixpoint function so assuming totality would be dumb lol
2025-03-27 05:10:07 +0100 <haskellbridge> <Bowuigi> EvanR it gets you the "lowest common denominator" of the members of all the semantics. On a lot of cases these are the most useful
2025-03-27 05:10:25 +0100 <haskellbridge> <Bowuigi> Unless you want to play around with bottoms, which is ok I guess
2025-03-27 05:10:43 +0100 <EvanR> an ultrafinitist interpretation might get you lower than the lowest common denominator
2025-03-27 05:11:01 +0100 <haskellbridge> <Bowuigi> A what
2025-03-27 05:11:14 +0100 <EvanR> for incredibly small values of infinity, such and such
2025-03-27 05:11:55 +0100Square(~Square@user/square) Square
2025-03-27 05:12:37 +0100 <haskellbridge> <Bowuigi> Doesn't totality forbid infinitely large values (excluding codata, which can still be encoded, tho not evaluated on its entirety) via Church-Rosser?
2025-03-27 05:12:51 +0100 <haskellbridge> <Bowuigi> Why do you need to constraint infinities?
2025-03-27 05:13:20 +0100 <EvanR> ultrafinitism would forbid infinite and most of the finite values
2025-03-27 05:13:58 +0100 <haskellbridge> <Bowuigi> Oh you sort of set a limit on how large your data can be?
2025-03-27 05:14:27 +0100 <haskellbridge> <Bowuigi> Like, "forbid all terms of size > 800"?
2025-03-27 05:14:29 +0100 <EvanR> yes, without giving an explicit limit, because someone might say "that plus one"
2025-03-27 05:14:45 +0100 <monochrom> May I invent ultraultrafinitism? It means since it doesn't believe in infinite values, it can't even forbid them. >:)
2025-03-27 05:14:56 +0100 <haskellbridge> <Bowuigi> Oh that's why you use infinities
2025-03-27 05:15:10 +0100 <EvanR> no you may not, because then you can't even invent ultraultrafinitism
2025-03-27 05:15:26 +0100 <EvanR> since you would be referring to things you're trying to forbid
2025-03-27 05:15:26 +0100 <haskellbridge> <Bowuigi> Just forbid codata and done
2025-03-27 05:15:48 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 05:16:05 +0100 <haskellbridge> <Bowuigi> I present ultrainfinitism, everything must be infinitely large, at least as large as the smallest infinity
2025-03-27 05:16:25 +0100 <EvanR> I usually force that now a days
2025-03-27 05:16:36 +0100 <EvanR> editing an image? the data is on an infinite plane thanks
2025-03-27 05:16:42 +0100 <haskellbridge> <Liamzee> finally
2025-03-27 05:16:44 +0100 <monochrom> I like ultrainfinitism.
2025-03-27 05:16:45 +0100 <haskellbridge> <Liamzee> ugh, 2 hours
2025-03-27 05:16:48 +0100 <haskellbridge> <Liamzee> didn't beat yin
2025-03-27 05:17:19 +0100 <EvanR> malloc never fails, infinite memory
2025-03-27 05:17:36 +0100 <EvanR> amazon delivers in 1/infinity days
2025-03-27 05:17:40 +0100 <haskellbridge> <Liamzee> (u -> ( (a -> b -> c) -> b -> a -> c) -> v) -> (u -> v)
2025-03-27 05:18:03 +0100 <haskellbridge> <Liamzee> so the answer is at flip flip flip, hmmm, not sure if anyone else is doing it and i'd spoil anyone?
2025-03-27 05:18:16 +0100 <EvanR> is this a djinn question
2025-03-27 05:18:41 +0100 <haskellbridge> <Liamzee> scroll up, yin posted the puzzle and their time "one afternoon"
2025-03-27 05:19:36 +0100 <EvanR> @djinn (u -> ( (a -> b -> c) -> b -> a -> c) -> v) -> (u -> v)
2025-03-27 05:19:36 +0100 <lambdabot> f a b = a b (\ c d e -> c e d)
2025-03-27 05:19:57 +0100 <EvanR> that's so much more useful than pointless
2025-03-27 05:20:19 +0100 <haskellbridge> <Bowuigi> It says half an afternoon for 'flip flip' to 'flip flip flip flip flip'
2025-03-27 05:20:29 +0100 <haskellbridge> <Liamzee> ack
2025-03-27 05:20:46 +0100 <haskellbridge> <Bowuigi> You need to flip it two more times in half the time
2025-03-27 05:20:53 +0100 <EvanR> :t fmap fmap fmap fmap fmap
2025-03-27 05:20:53 +0100 <lambdabot> Functor f => (a1 -> b) -> (a2 -> a1) -> f a2 -> f b
2025-03-27 05:20:55 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-27 05:22:15 +0100 <haskellbridge> <Bowuigi> It became contravariant at some point
2025-03-27 05:22:22 +0100 <monochrom> [exa]: We now have a new dreaded example for your minihm! flip flip flip flip flip ...
2025-03-27 05:22:24 +0100 <haskellbridge> <Liamzee> once you figure out the trick at 3 layers to 4, you don't need to do anything more
2025-03-27 05:22:39 +0100 <haskellbridge> <Bowuigi> Nvm I can't read
2025-03-27 05:22:53 +0100 <haskellbridge> <Liamzee> since it's (a -> (...) -> c) -> (a -> c)
2025-03-27 05:23:24 +0100 <haskellbridge> <Liamzee> in terms of types, the (...) is unused but propagates
2025-03-27 05:24:20 +0100 <haskellbridge> <Liamzee> flip is, let u = (a -> b -> c), v = b, w = (a -> c)
2025-03-27 05:25:17 +0100 <haskellbridge> <Liamzee> in u -> v -> w
2025-03-27 05:26:00 +0100 <haskellbridge> <Liamzee> plug in, (a -> (old b) -> c) -> (a -> c), with a unifying with u on the older form and c unifying with v on the older form
2025-03-27 05:26:09 +0100 <haskellbridge> <Liamzee> the actual challenge in the exercise tbh is explaining what's happening concisely
2025-03-27 05:28:21 +0100 <EvanR> and this is how derivation trees were invented
2025-03-27 05:30:01 +0100 <monochrom> No! This is how indentation was invented!
2025-03-27 05:30:44 +0100 <EvanR> indentation...
2025-03-27 05:31:12 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 05:31:38 +0100aforemny_(~aforemny@2001:9e8:6cdb:6d00:dc2e:87c9:d5a9:a75) aforemny
2025-03-27 05:32:25 +0100tabaqui(~tabaqui@167.71.80.236) tabaqui
2025-03-27 05:33:14 +0100aforemny(~aforemny@2001:9e8:6cc1:be00:edce:fe13:a80e:d4b5) (Ping timeout: 272 seconds)
2025-03-27 05:35:02 +0100JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-03-27 05:35:25 +0100 <EvanR> I can't indent in hexchat because tab changes widget focus
2025-03-27 05:36:05 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-27 05:42:13 +0100michalz(~michalz@185.246.207.197)
2025-03-27 05:45:08 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 05:46:12 +0100 <haskellbridge> <Bowuigi> That's why some people prefer spaces over tabs
2025-03-27 05:46:54 +0100 <haskellbridge> <Liamzee> ctrl shift u 0009 on gnome
2025-03-27 05:48:39 +0100 <haskellbridge> <Liamzee> no idea what it is in kde
2025-03-27 05:49:52 +0100 <haskellbridge> <Liamzee> do you still remember alt 0233 on windows?
2025-03-27 05:50:12 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 05:52:35 +0100Square2(~Square4@user/square) Square
2025-03-27 05:55:55 +0100chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2025-03-27 05:55:57 +0100Square(~Square@user/square) (Ping timeout: 244 seconds)
2025-03-27 05:56:30 +0100chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-03-27 06:00:15 +0100chiselfuse(~chiselfus@user/chiselfuse) (Read error: Connection reset by peer)
2025-03-27 06:00:15 +0100califax(~califax@user/califx) (Remote host closed the connection)
2025-03-27 06:00:15 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Read error: Connection reset by peer)
2025-03-27 06:00:29 +0100califax(~califax@user/califx) califx
2025-03-27 06:00:39 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-03-27 06:00:56 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 06:01:30 +0100chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-03-27 06:05:36 +0100zungi(~tory@user/andrewchawk) (Ping timeout: 264 seconds)
2025-03-27 06:05:56 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-27 06:08:57 +0100 <EvanR> lol yeah
2025-03-27 06:10:27 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection)
2025-03-27 06:13:13 +0100 <haskellbridge> <Liamzee> For some reason, I also remember typing a lot of 0252, but I can't remember why I'd use umlauted u
2025-03-27 06:16:42 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 06:21:19 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-27 06:22:00 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-03-27 06:22:36 +0100 <jackdk> The one I remember most s C-S-u 03bb
2025-03-27 06:23:59 +0100 <EvanR> cool, though it doesn't work in hexchat :(
2025-03-27 06:32:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 06:34:25 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-03-27 06:37:28 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-27 06:40:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 06:44:50 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 06:45:25 +0100 <monochrom> :)
2025-03-27 06:53:12 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2025-03-27 06:53:12 +0100gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2025-03-27 06:53:12 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Read error: Connection reset by peer)
2025-03-27 06:53:41 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2025-03-27 06:53:42 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2025-03-27 06:53:57 +0100gmg(~user@user/gehmehgeh) gehmehgeh
2025-03-27 06:55:38 +0100zungi(~tory@user/andrewchawk) andrewchawk
2025-03-27 06:55:47 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 07:00:57 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-03-27 07:08:37 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-03-27 07:09:25 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-03-27 07:09:53 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-03-27 07:11:22 +0100ensyde(~ensyde@2601:5c6:c200:6dc0::7f7c)
2025-03-27 07:11:30 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 07:13:07 +0100takuan(~takuan@d8D86B601.access.telenet.be)
2025-03-27 07:16:02 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 07:21:12 +0100zungi(~tory@user/andrewchawk) (Ping timeout: 264 seconds)
2025-03-27 07:24:34 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds)
2025-03-27 07:27:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 07:31:46 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-27 07:33:50 +0100aetepe(~aetepe@188.119.58.34) aetepe
2025-03-27 07:38:34 +0100aetepe(~aetepe@188.119.58.34) (Ping timeout: 260 seconds)
2025-03-27 07:42:46 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-27 07:49:32 +0100aetepe(~aetepe@188.119.58.34) aetepe
2025-03-27 07:50:08 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-27 07:54:08 +0100aetepe(~aetepe@188.119.58.34) (Ping timeout: 245 seconds)
2025-03-27 07:57:07 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2025-03-27 07:57:20 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2025-03-27 07:58:47 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
2025-03-27 08:00:03 +0100caconym(~caconym@user/caconym) (Quit: bye)
2025-03-27 08:00:51 +0100caconym(~caconym@user/caconym) caconym
2025-03-27 08:16:07 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2025-03-27 08:17:50 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-03-27 08:19:32 +0100 <haskellbridge> <Liamzee> in the early days of Haskell, before people figured out what a terrible idea abusing overloaded literals were
2025-03-27 08:19:54 +0100 <haskellbridge> <Liamzee> did anyone literally have a (Foo -> Bar) IsString?
2025-03-27 08:24:48 +0100 <Athas> Orphan instances are such a bad idea, but they are so easy and convenient.
2025-03-27 08:28:32 +0100 <haskellbridge> <Liamzee> it wouldn't be an orphan instance
2025-03-27 08:28:50 +0100 <haskellbridge> <Liamzee> it'd actually be more of an overlapping instances problem, tbh
2025-03-27 08:28:52 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-03-27 08:29:51 +0100acidjnk(~acidjnk@p200300d6e71c4f64d1428787ad85de6c.dip0.t-ipconnect.de) acidjnk
2025-03-27 08:30:20 +0100 <haskellbridge> <Liamzee> you can design an interface based around just, umm, building with overloaded strings and overlapping instances
2025-03-27 08:33:15 +0100 <haskellbridge> <Liamzee> i'm looking at Tomjaguarpaw's Opaleye, and...
2025-03-27 08:33:17 +0100 <haskellbridge> <Liamzee> https://github.com/tomjaguarpaw/haskell-opaleye/blob/master/Doc/Tutorial/TutorialBasic.lhs
2025-03-27 08:35:40 +0100aetepe(~aetepe@188.119.58.34) aetepe
2025-03-27 08:36:04 +0100 <haskellbridge> <Liamzee> the idea is so bad, i'm actually sort of surprised no one tried publishing "Acme-BreakTypeInferences" as a joke yet
2025-03-27 08:36:10 +0100 <haskellbridge> <Liamzee> erm, refering to my "let's make everything an overloaded string" idea
2025-03-27 08:37:24 +0100 <jackdk> Liamzee: https://hackage.haskell.org/package/acme-smuggler
2025-03-27 08:38:38 +0100 <haskellbridge> <Liamzee> no, i mean, I forget which version added it, but apparently you can now write your own custom type errors