4 ms·

Though make the type system sufficiently more expressive than Haskell's and you have to give up on type inference again... Though maybe you could restrict how

by Dewie3 11y ago

Though make the type system sufficiently more expressive than Haskell's and you have to give up on type inference again... Though maybe you could restrict how expressive the type system is on something like a module (Haskell module) level, so that you can have type inference if you give up on some power? I don't know.

Kutta 11y ago
Type inference doesn't somehow fail if we go beyond Haskell's type system. The inferable subset of the language remains inferable. Haskell already has inferable (Hindley-Milner) and uninferable (higher-rank polymorphism, GADTs) parts. If we go beyond Haskell's type system, it actually becomes crucial for productivity to have powerful type (and term) inference. Agda and Coq both have much more powerful inference than Haskell; it's just that don't bother with using it to realize Hindley-Milner-style annotation-free bindings, because there's little use for it in proof assistants.