Newest at the top
| 2026-04-03 18:14:51 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-03 18:13:59 +0000 | byorgey | (~byorgey@user/byorgey) byorgey |
| 2026-04-03 18:13:59 +0000 | byorgey | (~byorgey@155.138.238.211) (Changing host) |
| 2026-04-03 18:13:59 +0000 | byorgey | (~byorgey@155.138.238.211) |
| 2026-04-03 18:08:06 +0000 | confusedalex_ | confusedalex |
| 2026-04-03 18:08:06 +0000 | confusedalex | (~confuseda@user/confusedalex) (Ping timeout: 255 seconds) |
| 2026-04-03 18:07:15 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) (Ping timeout: 246 seconds) |
| 2026-04-03 18:07:02 +0000 | confusedalex_ | (~confuseda@user/confusedalex) confusedalex |
| 2026-04-03 17:59:31 +0000 | <dolio> | Like, there is T parametricity for a class of types if for all A in that class, functions T -> A must be constant, or something. |
| 2026-04-03 17:57:54 +0000 | <dolio> | You can probably generalize it so that it doesn't depend so much on relative 'size' too. |
| 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 |