| 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) |
| 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 +0100 | JuanDaugherty | (~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 +0100 | merijn | (~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 +0100 | merijn | (~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 +0100 | Square | (~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 +0100 | merijn | (~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 +0100 | merijn | (~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 |