[Haskell-cafe] Type-Level Programming

[C. McCann]

On Sat, Jun 26, 2010 at 6:55 PM, Erik de Castro Lopo
<mle+hs at mega-nerd.com> wrote:
> 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.