But I find such articles ridiculously hard to understand, especially system F (although I have been coding in #haskell for years).
Ironically, dependently-typed seem much simpler. In non-dependently-typed systems it's very hard to pinpoint the connections between types and terms. In dependently-typed systems, terms and types are the same thing.
Feeling many systems kinda approach the problem wrong, maybe we should have the constrained program synthesis way instead of typechecking-first everywhere by default - yeeeeeees very much.
Add comment