Newest at the top
| 2026-04-03 17:07:37 +0000 | <monochrom> | The analogy being: From inside Lean, the space of forall a. a -> [a] looks larger than what parametricity promises. |
| 2026-04-03 17:07:12 +0000 | <c_wraith> | Haskell is perfectly logical. It just doesn't require a consistent logic. |
| 2026-04-03 17:06:39 +0000 | <monochrom> | If you worry about Haskell not having a nice correspondence with logic (it has some correspondence, just messier), Lean would be a nicer example to look at. For Lean, I haven't thought about Skolem's paradox, but I have thought about parametricity. If you define a "foo :: a -> [a]" in Lean, you cannot prove that it's parametric from inside Lean. (You can and have to step outside and make it a meta-level theorem and proof.) |
| 2026-04-03 17:06:25 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) (Ping timeout: 245 seconds) |
| 2026-04-03 17:04:26 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 17:02:18 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-04-03 17:01:55 +0000 | <monochrom> | (Natural -> Bool) looks like an uncountable space, from inside the system. |
| 2026-04-03 17:00:29 +0000 | <monochrom> | Yes I think Skolem's paradox applies. Maybe with adjustments to technical details that don't really change the conclusion. |
| 2026-04-03 16:51:01 +0000 | machinedgod | (~machinedg@d172-219-48-230.abhsia.telus.net) machinedgod |
| 2026-04-03 16:37:29 +0000 | gentauro | I can see that Panic is going to be present at Zurihach 2026 |
| 2026-04-03 16:37:14 +0000 | <gentauro> | just wow !!! |
| 2026-04-03 16:37:08 +0000 | <gentauro> | https://abuseofnotation.github.io/category-theory-illustrated/ <- 🤯 |
| 2026-04-03 16:23:04 +0000 | rekahsoft | (~rekahsoft@76.67.111.168) rekahsoft |
| 2026-04-03 16:04:43 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 15:51:50 +0000 | <EvanR> | since haskell isn't logic and I'm not sure where it sits on first or second orderness, maybe not. But seems like a similar phenomenon |
| 2026-04-03 15:51:22 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-04-03 15:50:09 +0000 | <EvanR> | er skolem's paradox |
| 2026-04-03 15:50:04 +0000 | <EvanR> | does lowenheim skolem paradox have anything to do with the occasional "surprise" that haskell can have uncountable "sets", since this paradox relies on the idea of a first order logic |
| 2026-04-03 15:43:08 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 15:37:31 +0000 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 264 seconds) |
| 2026-04-03 15:35:14 +0000 | olivial | (~benjaminl@user/benjaminl) benjaminl |
| 2026-04-03 15:30:22 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-04-03 15:25:06 +0000 | olivial | (~benjaminl@user/benjaminl) (Ping timeout: 248 seconds) |
| 2026-04-03 15:24:50 +0000 | <monochrom> | (Just testing whether it's always the same string. >:) ) |
| 2026-04-03 15:24:30 +0000 | <yahb2> | ":>\164\&6\135-;\215\226?\250a\130\DC1\162\159\234\130\145p9\235\244YPY\DC1\241\240l\148{" |
| 2026-04-03 15:24:30 +0000 | <monochrom> | % Data.ByteString.Lazy.take 32 <$> Data.ByteString.Lazy.readFile "/dev/urandom" |
| 2026-04-03 15:23:21 +0000 | absurdvoid | (~absurdvoi@user/absurdvoid) absurdvoid |
| 2026-04-03 15:12:31 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-03 14:53:13 +0000 | craunts795335385 | (~craunts@152.32.99.2) |
| 2026-04-03 14:51:27 +0000 | Digit | (~user@user/digit) (Ping timeout: 255 seconds) |
| 2026-04-03 14:44:32 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 14:38:27 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 14:27:15 +0000 | somemathguy | (~somemathg@user/somemathguy) somemathguy |
| 2026-04-03 14:25:12 +0000 | qqq | (~qqq@185.54.23.237) (Remote host closed the connection) |
| 2026-04-03 14:14:38 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2026-04-03 14:14:38 +0000 | haritz | (~hrtz@140.228.70.141) (Changing host) |
| 2026-04-03 14:14:38 +0000 | haritz | (~hrtz@140.228.70.141) |
| 2026-04-03 14:07:22 +0000 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2026-04-03 14:05:23 +0000 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 252 seconds) |
| 2026-04-03 13:59:35 +0000 | Nosrep | (~jimothy@user/nosrep) Nosrep |
| 2026-04-03 13:57:40 +0000 | acidjnk_new | (~acidjnk@p200300d6e700e5029fa95e10e4e0754b.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-04-03 13:48:13 +0000 | <gentauro> | :) |
| 2026-04-03 13:47:29 +0000 | byorgey | (~byorgey@user/byorgey) (Quit: leaving) |
| 2026-04-03 13:42:18 +0000 | somemathguy | (~somemathg@user/somemathguy) (Ping timeout: 246 seconds) |
| 2026-04-03 13:34:38 +0000 | <tomsmeding> | gentauro: ^ |
| 2026-04-03 13:34:07 +0000 | <tomsmeding> | added it to the sandbox |
| 2026-04-03 13:33:51 +0000 | <yahb2> | "V4\205\ESC\247Kv\194\EOT\144\DLEf\165\211%\201\197&\156\ESC\190\CAN*\RS\CAN\215Fj\"\226n\CAN" |
| 2026-04-03 13:33:51 +0000 | <tomsmeding> | % Data.ByteString.Lazy.take 32 <$> Data.ByteString.Lazy.readFile "/dev/urandom" |
| 2026-04-03 13:33:45 +0000 | <yahb2> | <bye> |
| 2026-04-03 13:33:45 +0000 | <tomsmeding> | % :q |