26 Jun
2010
26 Jun
'10
7:27 p.m.
On Sat, Jun 26, 2010 at 6:55 PM, Erik de Castro Lopo
One problem with dependent types as I understand it is that type inference is not guaranteed to terminate.
Full type inference is undecidable in most interesting type systems anyway. It's possible for the simply-typed λ-calculus, but the best you can do beyond that is probably the Damas/Hindley/Milner algorithm which covers a (rather useful) subset of System F. This is the heart of Haskell's type inference, but some GHC extensions make type inference undecidable, such as RankNTypes. Type inference being undecidable is only a problem insofar as it requires adding explicit type annotations until the remaining types can be inferred. - C.