Newest at the top
| 2026-04-03 17:54:14 +0000 | <dolio> | Yeah. I recently heard about this, and like it better, because it seems closer to the intuitive idea of parametricity. |
| 2026-04-03 17:53:32 +0000 | <monochrom> | which is what I tell beginners if I'm not ready to tell the relational story. |
| 2026-04-03 17:53:01 +0000 | <monochrom> | Oh interesting, because "constant [over types]" is short for "the same code for all types". |
| 2026-04-03 17:50:35 +0000 | <dolio> | Instead of the relational way. |
| 2026-04-03 17:50:28 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-04-03 17:50:03 +0000 | confusedalex_ | confusedalex |
| 2026-04-03 17:49:52 +0000 | confusedalex_ | (~confuseda@user/confusedalex) confusedalex |
| 2026-04-03 17:49:47 +0000 | <dolio> | Where U is the 'universe'. |
| 2026-04-03 17:49:45 +0000 | confusedalex | (~confuseda@user/confusedalex) (Ping timeout: 245 seconds) |
| 2026-04-03 17:49:29 +0000 | <dolio> | Apparently that is a way of characterizing parametricity 'semantically', too. For all `A : U` then `f : U -> A` must be constant, basically. |
| 2026-04-03 17:49:28 +0000 | <lambdabot> | tellMe = tellMe . $map f |
| 2026-04-03 17:49:28 +0000 | <monochrom> | @free tellMe :: [a] -> Bool |
| 2026-04-03 17:49:13 +0000 | <EvanR> | lol |
| 2026-04-03 17:49:11 +0000 | <EvanR> | forall a . Bool ... |
| 2026-04-03 17:48:43 +0000 | <EvanR> | I was trying to figure out how to fix a -> Bool |
| 2026-04-03 17:48:38 +0000 | <monochrom> | I guess today's Haskell has "forall a -> Bool" as a middle ground. |
| 2026-04-03 17:48:35 +0000 | <EvanR> | yeah |
| 2026-04-03 17:47:36 +0000 | <dolio> | Yeah, that'd work. |
| 2026-04-03 17:47:18 +0000 | <monochrom> | Proxy a -> Bool! |
| 2026-04-03 17:47:09 +0000 | <monochrom> | haha |
| 2026-04-03 17:47:00 +0000 | <dolio> | If you have to provide an a, then the answer must be yes. :) |
| 2026-04-03 17:46:44 +0000 | <dolio> | It's really `tellMe :: forall a. Bool` |
| 2026-04-03 17:45:57 +0000 | <monochrom> | But I like dolio's. tellMe :: a -> Bool should be const True or const False, not tell you whether a is empty. |
| 2026-04-03 17:45:09 +0000 | <EvanR> | list makes it clear again |
| 2026-04-03 17:44:36 +0000 | <monochrom> | With parametricity, bar :: [a] implies bar = []. But what if you wrote "bar = if a is empty then [] else let x = choose an element from a in [x,x,x]" |
| 2026-04-03 17:44:13 +0000 | <EvanR> | oh |
| 2026-04-03 17:43:48 +0000 | <dolio> | Some are empty, some aren't. You don't get back the same 'yes/no' answer regardless of type. |
| 2026-04-03 17:43:26 +0000 | <dolio> | It's just not parametric over all types. |
| 2026-04-03 17:43:14 +0000 | <EvanR> | how does that help |
| 2026-04-03 17:43:05 +0000 | <monochrom> | Oh darn haha |
| 2026-04-03 17:42:53 +0000 | <dolio> | Excluded middle tells you whether a type is empty or not. |
| 2026-04-03 17:42:07 +0000 | <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:41:38 +0000 | <EvanR> | o_O |
| 2026-04-03 17:41:30 +0000 | <dolio> | Yeah. |
| 2026-04-03 17:41:25 +0000 | <EvanR> | excluded middle ruins parametricity? |
| 2026-04-03 17:40:57 +0000 | <dolio> | But in lean's case it's because people usually assume excluded middle and global choice. |
| 2026-04-03 17:40:41 +0000 | <monochrom> | Also of toString(). |
| 2026-04-03 17:40:20 +0000 | <EvanR> | didn't see the quotes at first |
| 2026-04-03 17:40:17 +0000 | <dolio> | Java is not parametric, either, because of `instanceof`. |
| 2026-04-03 17:39:57 +0000 | <EvanR> | oh a double not |
| 2026-04-03 17:38:59 +0000 | <EvanR> | but it comes up a lot when trying to explain haskell polymorphism |
| 2026-04-03 17:38:48 +0000 | <EvanR> | I might be too far gone, I never think of stuff like that xD |
| 2026-04-03 17:38:48 +0000 | <int-e> | dolio: nice use of `not` in a sentence :) |
| 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 |