Newest at the top
| 2026-04-03 17:34:17 +0000 | <monochrom> | ∀x. foo x = replicate (length (foo ()) x |
| 2026-04-03 17:33:29 +0000 | <monochrom> | That "∃n" is annoying and elusive, especially since we know exactly how to obtain that n. It's length (foo ()). |
| 2026-04-03 17:33:27 +0000 | <EvanR> | ok, I messed up because it's not just some arbitrary n, it's the same n for all types |
| 2026-04-03 17:32:22 +0000 | <monochrom> | Here is how your idea is not too far off from the abstract equation. Suppose you say "∃n. ∀x. foo x = replicate n x". |
| 2026-04-03 17:32:13 +0000 | craunts795335385 | (~craunts@152.32.99.2) (Quit: The Lounge - https://thelounge.chat) |
| 2026-04-03 17:30:34 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:22:02 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-04-03 17:21:59 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-03 17:21:57 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:21:28 +0000 | <monochrom> | Suppose you know from testing foo () = [(),()], and now you wonder about foo 4. Choose f = const 4. So map (const 4) (foo ()) = foo (const 4 ()), so [4,4] = foo 4. |
| 2026-04-03 17:21:26 +0000 | puke | (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:21:17 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-03 17:21:08 +0000 | tromp | (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 17:19:59 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:19:14 +0000 | puke | (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:17:42 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:16:57 +0000 | puke | (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:16:56 +0000 | <monochrom> | If you add the wording "that 'some number' is the same for all inputs for all types", then it's right on. |
| 2026-04-03 17:16:01 +0000 | <monochrom> | That's abstract. But if you try one single test case "foo ()" and get [(), ()], then you know that foo x = [x,x] for all x for all types. |
| 2026-04-03 17:16:01 +0000 | <c_wraith> | I mean... yes. that *is* the same as saying it's producing some number of copies of the input, though it's expressed in a slightly funny way |
| 2026-04-03 17:15:27 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:15:26 +0000 | <EvanR> | o_O |
| 2026-04-03 17:15:17 +0000 | <lambdabot> | $map f . foo = foo . f |
| 2026-04-03 17:15:16 +0000 | <monochrom> | @free foo :: a -> [a] |
| 2026-04-03 17:14:56 +0000 | <EvanR> | what is the free theorem, that foo has to yield some number of copies of the input |
| 2026-04-03 17:13:33 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-03 17:13:00 +0000 | puke | (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:12:59 +0000 | <monochrom> | Err I misspoke. For each individual foo that you know the implementation of, you can prove the free theorem for that foo based on its implementation. But you can't within Lean prove the free theorem for the type "forall a. a -> [a]". |
| 2026-04-03 17:12:39 +0000 | puke | (~puke@user/puke) puke |
| 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 |