wren ng thornton wren at freegeek.org
Sat Jun 26 23:55:50 EDT 2010

```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?
>>
>>
>> "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.

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
```