Newest at the top
| 2026-04-03 17:38:05 +0000 | <monochrom> | anything that violates free theorems. |
| 2026-04-03 17:37:48 +0000 | <dolio> | E.G. `f : ∀a. a -> a` where `f` is the identity on most types, but `not` on `Bool`. |
| 2026-04-03 17:37:41 +0000 | <monochrom> | foo x = if x is an Int and x==4 then [1,2,3,x,x^2,42,67] else [x,x,x] |
| 2026-04-03 17:37:23 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-03 17:37:17 +0000 | <EvanR> | a function that's not parametric |
| 2026-04-03 17:37:07 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2026-04-03 17:37:03 +0000 | <EvanR> | what's a "non-parametric function" besides the obvious |
| 2026-04-03 17:36:25 +0000 | <monochrom> | The abstract equation merely generalizes from const x to arbitrary f. |
| 2026-04-03 17:36:18 +0000 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-04-03 17:36:10 +0000 | <lambdabot> | a -> [a] |
| 2026-04-03 17:36:09 +0000 | <int-e> | :t \x -> [undefined, x, undefined] |
| 2026-04-03 17:36:05 +0000 | <monochrom> | ∀x. foo x = map (const x) (foo ()). Now @pointfree to get: foo . const x = map (const x) . foo |
| 2026-04-03 17:34:55 +0000 | <monochrom> | But I can simplify "replicate (length (foo ()) x" to "map (const x) (foo ())". Bonus: Now it covers infinite lists too! |
| 2026-04-03 17:34:35 +0000 | <dolio> | Common lean practice is to assume there are non-parametric functions. |
| 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. |