Logs: liberachat/#haskell
| 2026-04-03 13:42:18 | × | somemathguy quits (~somemathg@user/somemathguy) (Ping timeout: 246 seconds) |
| 2026-04-03 13:47:29 | × | byorgey quits (~byorgey@user/byorgey) (Quit: leaving) |
| 2026-04-03 13:48:13 | <gentauro> | :) |
| 2026-04-03 13:57:40 | × | acidjnk_new quits (~acidjnk@p200300d6e700e5029fa95e10e4e0754b.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-04-03 13:59:35 | → | Nosrep joins (~jimothy@user/nosrep) |
| 2026-04-03 14:05:23 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 252 seconds) |
| 2026-04-03 14:07:22 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 2026-04-03 14:14:38 | → | haritz joins (~hrtz@140.228.70.141) |
| 2026-04-03 14:14:38 | × | haritz quits (~hrtz@140.228.70.141) (Changing host) |
| 2026-04-03 14:14:38 | → | haritz joins (~hrtz@user/haritz) |
| 2026-04-03 14:25:12 | × | qqq quits (~qqq@185.54.23.237) (Remote host closed the connection) |
| 2026-04-03 14:27:15 | → | somemathguy joins (~somemathg@user/somemathguy) |
| 2026-04-03 14:38:27 | × | tromp quits (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 14:44:32 | → | tromp joins (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 14:51:27 | × | Digit quits (~user@user/digit) (Ping timeout: 255 seconds) |
| 2026-04-03 14:53:13 | → | craunts795335385 joins (~craunts@152.32.99.2) |
| 2026-04-03 15:12:31 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-03 15:23:21 | → | absurdvoid joins (~absurdvoi@user/absurdvoid) |
| 2026-04-03 15:24:30 | <monochrom> | % Data.ByteString.Lazy.take 32 <$> Data.ByteString.Lazy.readFile "/dev/urandom" |
| 2026-04-03 15:24:30 | <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:50 | <monochrom> | (Just testing whether it's always the same string. >:) ) |
| 2026-04-03 15:25:06 | × | olivial quits (~benjaminl@user/benjaminl) (Ping timeout: 248 seconds) |
| 2026-04-03 15:30:22 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 2026-04-03 15:35:14 | → | olivial joins (~benjaminl@user/benjaminl) |
| 2026-04-03 15:37:31 | × | Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 264 seconds) |
| 2026-04-03 15:43:08 | × | tromp quits (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 15:50:04 | <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:50:09 | <EvanR> | er skolem's paradox |
| 2026-04-03 15:51:22 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 2026-04-03 15:51:50 | <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 16:04:43 | → | tromp joins (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 16:23:04 | → | rekahsoft joins (~rekahsoft@76.67.111.168) |
| 2026-04-03 16:37:08 | <gentauro> | https://abuseofnotation.github.io/category-theory-illustrated/ <- 🤯 |
| 2026-04-03 16:37:14 | <gentauro> | just wow !!! |
| 2026-04-03 16:37:29 | gentauro | I can see that Panic is going to be present at Zurihach 2026 |
| 2026-04-03 16:51:01 | → | machinedgod joins (~machinedg@d172-219-48-230.abhsia.telus.net) |
| 2026-04-03 17:00:29 | <monochrom> | Yes I think Skolem's paradox applies. Maybe with adjustments to technical details that don't really change the conclusion. |
| 2026-04-03 17:01:55 | <monochrom> | (Natural -> Bool) looks like an uncountable space, from inside the system. |
| 2026-04-03 17:02:18 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2026-04-03 17:04:26 | × | tromp quits (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-03 17:06:25 | × | jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 245 seconds) |
| 2026-04-03 17:06:39 | <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:07:12 | <c_wraith> | Haskell is perfectly logical. It just doesn't require a consistent logic. |
| 2026-04-03 17:07:37 | <monochrom> | The analogy being: From inside Lean, the space of forall a. a -> [a] looks larger than what parametricity promises. |
| 2026-04-03 17:12:39 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:12:59 | <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:13:00 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:13:33 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-03 17:14:56 | <EvanR> | what is the free theorem, that foo has to yield some number of copies of the input |
| 2026-04-03 17:15:16 | <monochrom> | @free foo :: a -> [a] |
| 2026-04-03 17:15:17 | <lambdabot> | $map f . foo = foo . f |
| 2026-04-03 17:15:26 | <EvanR> | o_O |
| 2026-04-03 17:15:27 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:16:01 | <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:16:01 | <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:56 | <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:57 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:17:42 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:19:14 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:19:59 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:21:08 | → | tromp joins (~textual@2001:1c00:340e:2700:f5b2:b468:1c7d:8570) |
| 2026-04-03 17:21:17 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-03 17:21:26 | × | puke quits (~puke@user/puke) (Max SendQ exceeded) |
| 2026-04-03 17:21:28 | <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:57 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:21:59 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-03 17:22:02 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-04-03 17:30:34 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:32:13 | × | craunts795335385 quits (~craunts@152.32.99.2) (Quit: The Lounge - https://thelounge.chat) |
| 2026-04-03 17:32:22 | <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:33:27 | <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:33:29 | <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:34:17 | <monochrom> | ∀x. foo x = replicate (length (foo ()) x |
| 2026-04-03 17:34:35 | <dolio> | Common lean practice is to assume there are non-parametric functions. |
| 2026-04-03 17:34:55 | <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:36:05 | <monochrom> | ∀x. foo x = map (const x) (foo ()). Now @pointfree to get: foo . const x = map (const x) . foo |
| 2026-04-03 17:36:09 | <int-e> | :t \x -> [undefined, x, undefined] |
| 2026-04-03 17:36:10 | <lambdabot> | a -> [a] |
| 2026-04-03 17:36:18 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 268 seconds) |
| 2026-04-03 17:36:25 | <monochrom> | The abstract equation merely generalizes from const x to arbitrary f. |
| 2026-04-03 17:37:03 | <EvanR> | what's a "non-parametric function" besides the obvious |
| 2026-04-03 17:37:07 | × | puke quits (~puke@user/puke) (Quit: puke) |
| 2026-04-03 17:37:17 | <EvanR> | a function that's not parametric |
| 2026-04-03 17:37:23 | → | puke joins (~puke@user/puke) |
| 2026-04-03 17:37:41 | <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:48 | <dolio> | E.G. `f : ∀a. a -> a` where `f` is the identity on most types, but `not` on `Bool`. |
| 2026-04-03 17:38:05 | <monochrom> | anything that violates free theorems. |
| 2026-04-03 17:38:48 | <int-e> | dolio: nice use of `not` in a sentence :) |
| 2026-04-03 17:38:48 | <EvanR> | I might be too far gone, I never think of stuff like that xD |
| 2026-04-03 17:38:59 | <EvanR> | but it comes up a lot when trying to explain haskell polymorphism |
| 2026-04-03 17:39:57 | <EvanR> | oh a double not |
| 2026-04-03 17:40:17 | <dolio> | Java is not parametric, either, because of `instanceof`. |
| 2026-04-03 17:40:20 | <EvanR> | didn't see the quotes at first |
| 2026-04-03 17:40:41 | <monochrom> | Also of toString(). |
| 2026-04-03 17:40:57 | <dolio> | But in lean's case it's because people usually assume excluded middle and global choice. |
| 2026-04-03 17:41:25 | <EvanR> | excluded middle ruins parametricity? |
| 2026-04-03 17:41:30 | <dolio> | Yeah. |
| 2026-04-03 17:41:38 | <EvanR> | o_O |
| 2026-04-03 17:42:07 | <monochrom> | So on parametricity homework I pose "if we listened to Java people, then foo :: Show a => a -> [a], now write your foo so that foo () = [(),()] but foo 4 = [1,2,3]" |
| 2026-04-03 17:42:53 | <dolio> | Excluded middle tells you whether a type is empty or not. |
All times are in UTC.