[Haskell-cafe] Type-Level Programming

[wren ng thornton]

Andrew Coppin wrote:
> Stephen Tetley wrote:
>> On 26 June 2010 08:07, Andrew Coppin <andrewcoppin at btinternet.com> 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