Newest at the top
| 2026-06-30 11:57:45 +0000 | fgarcia | (~lei@user/fgarcia) fgarcia |
| 2026-06-30 11:55:35 +0000 | fgarcia | (~lei@user/fgarcia) (Ping timeout: 252 seconds) |
| 2026-06-30 11:55:01 +0000 | lynxx_ | (~lynxx_@2001:9e8:3bcd:2200:997c:8365:c7f6:f178) |
| 2026-06-30 11:44:09 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-30 11:43:25 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-30 11:42:57 +0000 | <tomsmeding> | depending on how deep you want to dive into this :p |
| 2026-06-30 11:42:34 +0000 | <tomsmeding> | fp: ^ another resource |
| 2026-06-30 11:40:51 +0000 | <tomsmeding> | now I want to know the most _what_ type system System Fω is lol |
| 2026-06-30 11:40:15 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-30 11:39:55 +0000 | <tomsmeding> | > System Fω stands as one of the most type systems in the theoretical foundations of programming languages |
| 2026-06-30 11:39:19 +0000 | <gentauro> | tomsmeding: -> https://sdiehl.github.io/typechecker-zoo/system-f-omega/system-f-omega.html ;) |
| 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) |