Re: [Haskell-cafe] Type-Level Programming

Andrew Coppin wrote:

Stephen Tetley wrote:

...

On 26 June 2010 08:07, Andrew Coppin wrote:

...

Out of curiosity, what the hell does "dependently typed" mean anyway?

How about:

"The result type of a function may depend on the argument value" (rather than just the argument type)

Hmm. This sounds like one of those things where the idea is simple, but the consequences are profound...

The simplest fully[1] dependently typed formalism is one of the many variants of LF. LF is an extension of the simply typed lambda calculus, extending the arrow type constructor to be ((x:a) -> b) where the variable x is bound to the argument value and has scope over b. In order to make use of this, we also allow type constructors with dependent kinds, for example with the type family (P : A -> *) we could have a function (f : (x:A) -> P x). Via Curry--Howard isomorphism this gives us first-order intuitionistic predicate calculus (whereas STLC is 1st-order propositional calculus). The switch from atomic propositions to predicates is where the profundity lies. A common extension to LF is to add dependent pairs, generalizing the product type constructor to be ((x:a) * b), where the variable x is bound to the first component of the pair and has scope over b. This extension is rather trivial in the LF setting, but it can cause unforeseen complications in more complex formalisms. Adding dependencies is orthogonal to adding polymorphism or to adding higher-orderness. Though "orthogonal" should probably be said with scare-quotes. In the PTS presentation of Barendregt's lambda cube these three axes are indeed syntactically orthogonal. However, in terms of formal power, the lambda cube isn't really a cube as such. There are numerous shortcuts and wormholes connecting far reaches in obscure non-Euclidean ways. The cube gives a nice overview to start from, but don't confuse the map for the territory. One particular limitation of LF worth highlighting is that, even though term-level values may *occur* in types, they may not themselves *be* types. That is, in LF, we can't have any function like (g : (x:a) -> x). In the Calculus of Constructions (CC)[2], this restriction is lifted in certain ways, and that's when the distinction between term-level and type-level really breaks down. Most current dependently typed languages (Coq, Agda, Epigram, LEGO, NuPRL) are playing around somewhere near here, whereas older languages tended to play around closer to LF or ITT (e.g., Twelf). And as a final note, GADTs and type families are forms of dependent types, so GHC Haskell is indeed a dependently typed language (of sorts). They're somewhat kludgy in Haskell because of the way they require code duplication for term-level and type-level definitions of "the same" function. In "real" dependently typed languages it'd be cleaner to work with these abstractions since we could pass terms into the type level directly, however that cleanliness comes with other burdens such as requiring that all functions be provably terminating. Managing to balance cleanliness and the requirements of type checking is an ongoing research area. (Unless you take the Cayenne route and just stop caring about whether type checking will terminate :) [1] Just as Hindley--Milner is an interesting stopping point between STLC and System F, there are also systems between STLC and LF. [2] In terms of formal power: CC == F_omega + LF == ITT + SystemF. -- Live well, ~wren