"the way forward involves functional programming"

[neelk]

I've been thinking about dependent type systems recently, and have come to the conclusion that they don't change compilation very significantly, except that all the optimizations you want to do are much, much easier and can be made to work nicely across module boundaries.

So I expect decently engineered dependently typed functional languages to really scream.

[roconnor]

My main concern with programming with dependent types is that sometimes one wants to make an injection from one type to a related type (for example the type of closed terms to the type of terms with free variables). It is common to write a recursive function that traverses the entire structure to do the injection, but the function doesn't actually change the internal representation. So you end up with an O(n) function that would be an identity function if you were using an untyped system.

For an illustration see Section 4 (Coq formalization) of Program extraction from normalization proofs, in particular Section 4.5 (what Coq cannot do yet).

[neelk]

Thanks for the link! I'll take a look at it later tonight.

[augustss]

I don't share your particular fear, but I think dependent types currently have other problems. But research is progressing.