19 ms·
I think in dependently typed programming languages and theorem proves. As I understand it, even System F (like Haskell) benefits, no?
by guerrilla 1y ago
I think in dependently typed programming languages and theorem proves. As I understand it, even System F (like Haskell) benefits, no?
- cubefox 1y agoI guess in System F, if a function f accepts a complex type A, and another function g returns a complex type B, both types could involve type variables. Then for the compiler to check whether the expression f(g) is valid, it (the compiler) needs to determine whether a unification of A and B is possible. Not sure though.
- dunham 1y agoAs I understand it, dependent type theory requires higher order unification, which is undecidable. So they typically use bidirectional type checking instead of Hindley Milner. With bidirection type checking, I think it only needs the unification when solving inserted implicits. So a plain dependent type theory wouldn't need it, but once you add implicit parameters, you do need it. They usually use pattern unification, which solves a subset of higher order unification problems, for those unification problems.