Newest at the top
| 2026-04-15 18:34:17 +0000 | <EvanR> | it seems that an early (?) attitude of hilbert, continually faced with mathematical surprises while trying to carry out a formalist agenda, imagined a distinction between "real math" and "ideal math". Someone like cantor would report the discover of various infinities. It would be the formalists job to eventually account for this in the ideal formal version. Like their doing empirical science |
| 2026-04-15 18:33:28 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 18:28:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-15 18:27:37 +0000 | ft | (~ft@p508db287.dip0.t-ipconnect.de) ft |
| 2026-04-15 18:26:26 +0000 | <monochrom> | Recently I learned a bit of non-standard real analysis. We can just s/exotic/non-standard/. Wooo infinitestimals and extra bottoms and infinite lists... |
| 2026-04-15 18:24:08 +0000 | misterfish | (~misterfis@84.53.85.146) misterfish |
| 2026-04-15 18:23:50 +0000 | <EvanR> | all the proofs can go through formally and haskell is just an exotic model |
| 2026-04-15 18:21:51 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 18:21:40 +0000 | <monochrom> | I can imagine Bob Harper looking at all these annoyances and conclude "forget Haskell". :) |
| 2026-04-15 18:18:25 +0000 | Square2 | (~Square@user/square) Square |
| 2026-04-15 18:17:38 +0000 | Square2 | (~Square@user/square) (Remote host closed the connection) |
| 2026-04-15 18:16:04 +0000 | <monochrom> | Unfortunately Z has fewer bottoms than Either () Z too. Either Void Z should work, but it's a hack. |
| 2026-04-15 18:16:02 +0000 | Square2 | (~Square@user/square) Square |
| 2026-04-15 18:11:14 +0000 | <monochrom> | Err no, I have to re-think it. |
| 2026-04-15 18:11:09 +0000 | alter2000 | (~alter2000@user/alter2000) alter2000 |
| 2026-04-15 18:10:09 +0000 | <monochrom> | Whereas for less mind-boggling examples like "data Z = Z | S Z" you have the expected isomorphism again! So all is not lost. |
| 2026-04-15 18:08:16 +0000 | <monochrom> | or at least writing the book with that assumption. |
| 2026-04-15 18:07:54 +0000 | craunts795335385 | (~craunts@152.32.99.2) (Client Quit) |
| 2026-04-15 18:07:51 +0000 | <monochrom> | This is something TaPL won't bring up because the author is from SML not Haskell. |
| 2026-04-15 18:06:59 +0000 | <monochrom> | because that difference then carries over to "data X = X [X]" and "newtype Y = Y [Y]". Then X is not quite isomorphic to [X]. |
| 2026-04-15 18:06:20 +0000 | <monochrom> | Do you already know the denotational difference between "data D = D Int" and "newtype N = N Int"? |
| 2026-04-15 18:06:14 +0000 | <EvanR> | \case {Left () -> Nil; Right (x,xs) -> Cons x xs} |
| 2026-04-15 18:05:51 +0000 | <EvanR> | \case {Nil -> Left (); Cons x xs -> Right (x,xs)} |
| 2026-04-15 18:03:34 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 256 seconds) |
| 2026-04-15 18:03:31 +0000 | <janus> | monochrom: but 'data' still allows for recursion right? so how is that recursion described formally? is it neither iso nor equi? |
| 2026-04-15 18:03:29 +0000 | craunts795335385 | (~craunts@152.32.99.2) |
| 2026-04-15 18:02:47 +0000 | <monochrom> | Yeah. |
| 2026-04-15 18:02:42 +0000 | <EvanR> | so IntList and 1 + Int x IntList |
| 2026-04-15 18:02:22 +0000 | craunts795335385 | (~craunts@152.32.99.2) (Quit: The Lounge - https://thelounge.chat) |
| 2026-04-15 18:01:36 +0000 | <janus> | that is what they call fold/unfold |
| 2026-04-15 18:01:31 +0000 | <janus> | the TAPL book talks about a an isomorphism between the type without it's own definition pasted in, and the one that has that replacement done |
| 2026-04-15 18:01:10 +0000 | <monochrom> | With "data" you don't in Haskell, but you still do back in SML (generally strict languages). |
| 2026-04-15 18:00:40 +0000 | <monochrom> | Yeah with newtype you have that isomorphism. |
| 2026-04-15 18:00:25 +0000 | <EvanR> | morally |
| 2026-04-15 18:00:09 +0000 | <EvanR> | Mu f `iso` f (Mu f) makes sense because it's a newtype |
| 2026-04-15 17:59:47 +0000 | <EvanR> | isomorphism between what and what |
| 2026-04-15 17:59:30 +0000 | <monochrom> | Yes Haskell does iso-recursive, doesn't do equi-recursive. |
| 2026-04-15 17:59:10 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 17:57:59 +0000 | <janus> | ncf: in 'data IntList = Nil | Cons Int IntList', what would be the witnesses of the isomorphism? |
| 2026-04-15 17:56:34 +0000 | ouilemur | (~jgmerritt@user/ouilemur) (Quit: WeeChat 4.9.0) |
| 2026-04-15 17:56:28 +0000 | alter2000 | (~alter2000@user/alter2000) (Ping timeout: 244 seconds) |
| 2026-04-15 17:51:49 +0000 | Enrico63 | (~Enrico63@host-79-42-237-9.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-04-15 17:46:27 +0000 | <janus> | while in haskell, they're not. so now i have to juggle variants and recursiveness at the same time |
| 2026-04-15 17:45:45 +0000 | <janus> | i am confused by variants being anonymous in TAPL, i guess.. |
| 2026-04-15 17:45:07 +0000 | <janus> | it's just that in TAPL, they say that unfold/fold are primitives , and if they should work with recursive records in haskell, i don't see how it fits with what you're saying, because there is no name for the unwrapped Mu |
| 2026-04-15 17:44:11 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 252 seconds) |
| 2026-04-15 17:42:45 +0000 | <ncf> | e.g. in data Mu f = Mu { unMu :: f (Mu f) } you have Mu f ≃ f (Mu f) up to an isomorphism (witnessed by Mu and unMu), not an actual type equality |
| 2026-04-15 17:41:53 +0000 | <ncf> | janus: wdym? haskell's recursive types are isorecursive |
| 2026-04-15 17:39:40 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 17:27:33 +0000 | jle` | (~jle`@2603:8001:3b00:11:4360:f9b:cc52:4598) jle` |