Newest at the top
| 2026-06-30 11:21:02 +0000 | <fp> | Interesting, I'll have to read |
| 2026-06-30 11:20:40 +0000 | <tomsmeding> | and the terminology when you read about this stuff tends to assume some knowledge about basic type theory |
| 2026-06-30 11:20:07 +0000 | <tomsmeding> | both simply typed lambda calculus and dependently-typed calculi (type theory) have much theory and literature devoted to them; system F and Haskell are a bit in the middle |
| 2026-06-30 11:19:25 +0000 | <tomsmeding> | https://en.wikipedia.org/wiki/System_F |
| 2026-06-30 11:19:21 +0000 | <tomsmeding> | oh I guess this is just system F |
| 2026-06-30 11:18:33 +0000 | <tomsmeding> | there may well be resources that explain this in more detail for haskell specifically, but I don't know them |
| 2026-06-30 11:18:11 +0000 | xff0x | (~xff0x@2405:6580:b080:900:f8e0:a6ee:fc93:d765) |
| 2026-06-30 11:17:58 +0000 | <tomsmeding> | fp: re manual, I don't think the GHC manual explains any of this since it generally assumes you know the underlying theory |
| 2026-06-30 11:11:51 +0000 | <tomsmeding> | but when thinking about meaning and behaviour in the type system, I think this perspective is much more precise |
| 2026-06-30 11:11:26 +0000 | <tomsmeding> | now, when you actually want to execute this stuff and be fast-ish, you indeed start thinking about dynamic dispatch and polymorphic code and stuff |
| 2026-06-30 11:10:43 +0000 | <tomsmeding> | on the other hand, (g1 :: forall a. Num a => Bool -> a) and (g2 :: Bool -> (forall a. Num a => a)) are the same up to argument ordering: they both take 3 arguments, just in a different order |
| 2026-06-30 11:10:43 +0000 | <fp> | You know, there's probably a manual page I should read about this |
| 2026-06-30 11:10:03 +0000 | <tomsmeding> | as such (f1 :: forall a. Num a => a -> Bool) and (f2 :: (forall a. Num a => a) -> Bool) are very different: f1 takes 3 arguments, f2 takes 1 |
| 2026-06-30 11:09:32 +0000 | <tomsmeding> | f :: forall a. Num a => Bool -> a takes 3 arguments: a type 'a', a dictionary 'Num a', and a 'Bool' |
| 2026-06-30 11:09:27 +0000 | <fp> | I guess in my head, forall is a thing that creates dynamic dispatch on the backend |
| 2026-06-30 11:09:07 +0000 | <tomsmeding> | I'm not sure where your thoughts are / where you're stuck (if you are), but in case you're not familiar with that view, you can see "forall" as just another argument |
| 2026-06-30 11:08:26 +0000 | <tomsmeding> | those two functions are just the other way round, I'm not sure where type erasure comes in |
| 2026-06-30 11:07:51 +0000 | <fp> | Mm, then could it be `f :: forall a. Num a => a -> Bool` is what I said and `g:: forall a. Num a => Bool -> a` is type erasure? |
| 2026-06-30 11:06:39 +0000 | <tomsmeding> | fp: "a function" -- which function? It matters on which side the forall stands :) |
| 2026-06-30 11:04:12 +0000 | fun-safe-math | (~fun-safe-@97-120-35-225.ptld.qwest.net) fun-safe-math |
| 2026-06-30 11:04:05 +0000 | tremon | (~tremon@83-80-159-219.cable.dynamic.v4.ziggo.nl) tremon |
| 2026-06-30 11:02:45 +0000 | <fp> | does `forall a. Num a` mean that a single monomorphization of a function will polymorphically accept any Num a => a ? |
| 2026-06-30 11:02:17 +0000 | fun-safe-math | (~fun-safe-@97-120-35-225.ptld.qwest.net) () |
| 2026-06-30 11:00:25 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-30 10:59:24 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-30 10:57:48 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2026-06-30 10:57:19 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-30 10:55:12 +0000 | <tomsmeding> | there are fewer Ints than "arbitrary Num values", but if you have to _take_ an arbitrary Num value, there's less you can do than if you know you're getting an Int |
| 2026-06-30 10:54:51 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-30 10:53:49 +0000 | <tomsmeding> | but ((forall a. Num a => a) -> Bool) <= (Int -> Bool) |
| 2026-06-30 10:53:21 +0000 | <tomsmeding> | Int <= (forall a. Num a => a) [here '<=' is "more specific"], hence (Bool -> Int) <= (Bool -> forall a. Num a => a) = (forall a. Num a => Bool -> a) |
| 2026-06-30 10:53:00 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-30 10:52:34 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-30 10:52:12 +0000 | <tomsmeding> | you can see the subtyping version in Haskell too, even though Haskell does not, by the usual terminology, have subtyping: polymorphism has similar behaviour |
| 2026-06-30 10:51:40 +0000 | <fp> | I'v fallen down a bit of a rabbit hole of people talking about wacky algebras and type-level programming, and stuff like this comes up |
| 2026-06-30 10:50:45 +0000 | <fp> | Ok interesting thank you |
| 2026-06-30 10:50:16 +0000 | <tomsmeding> | with the category theory one, the thing that "varies" is the direction of movement along the arrow, I guess? I'm not a category theorist |
| 2026-06-30 10:49:52 +0000 | <tomsmeding> | with the type systems one, the thing that varies is the specificity along the subtyping relation ("making something more 'sub'") |
| 2026-06-30 10:49:25 +0000 | <tomsmeding> | hence 'a -> b' is said to be covariant in b (because b' <= b ==> a -> b' <= a -> b), and contravariant in a (because a' <= a ==> a -> b <= a' -> b) |
| 2026-06-30 10:49:23 +0000 | <fp> | Mm I see |
| 2026-06-30 10:48:25 +0000 | <tomsmeding> | but if you're expecting a function A' -> B, then a function A -> B also works, as passing an A' to that is fine by subtyping |
| 2026-06-30 10:47:45 +0000 | <tomsmeding> | because whenever B -> A works, getting a more precise A out (i.e. an A') would be acceptable |
| 2026-06-30 10:47:29 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-30 10:47:20 +0000 | <tomsmeding> | but then if you think about it, B -> A' should be a subtype of B -> A, but A -> B should be a subtype of A' -> B |
| 2026-06-30 10:46:49 +0000 | <tomsmeding> | co(ntra)variance in type systems relates to subtyping, where the idea is that a subtype A' of A is to be accepted wherever A is |
| 2026-06-30 10:46:17 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-30 10:46:00 +0000 | <tomsmeding> | a covariant functor has fmap : (a -> b) -> T a -> T b; a contravariant functor has fmap : (a -> b) -> T b -> T a |
| 2026-06-30 10:45:33 +0000 | <tomsmeding> | fp: I think there are two different notions of co(ntra)variant here: one is that of a co(ntra) variant functor, and the other is that of co(ntra)variance in type systems |
| 2026-06-30 10:44:12 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-30 10:41:32 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |