Another typing question

C T McBride
Wed, 6 Aug 2003 11:15:13 +0100 (BST)


On Tue, 5 Aug 2003, Jon Cast wrote:

> Actually, on second thought, I think this could be simplified to: if we
> have dependant types, then either there is a type which cannot be used
> in a dependant type, or for every polymorphic function there is a type
> it cannot be applied at.

This is why most sensible dependent type theories have a hierarchy of
universes behind the scenes. You can think of * in Haskell as the lowest
universe, inhabited by types. Kinds live in the next level up. Haskell
stops there, but there's no need to. The point is that objects polymorphic
in level n things belong to level n+1. This way, no paradox, no
nontermination, entirely decidable typechecking. One benefit of presenting
this hierarchy in a uniform manner is that it's perfectly feasible to
specify operations under which each level is closed: universal and
existential quantification, all your usual polymorphic data structures, so
that [Int] is at level 0, whilst [*] is at level 1.

Sure, you can't apply `the' polymorphic identity function at its own
polymorphic type, but you can apply the level 1 polymorphic identity at
the type of the level 0 polymorphic identity. You write id id. The machine
can handle all the book-keeping of levels, so you never need to see those
details, unless you do attempt to create a genuine paradox.

I'm working on dependently typed programming because I can see some
benefits for declarative programming from the way that more expressive
types allow you to tell the typechecker more of the structure you have in
mind when you write a program---the typechecker may then help you write it
correctly. Other benefits include the static checking of data structure
invariants (cashing out potentially as code which needs fewer run-time
checks to be safe/correct), guaranteed absence of run-time errors,
totality (should you choose to work in the terminating fragment) and
sometimes even correctness (if your type is speccific enough).

I sometimes get the impression that lots of functional programmers have
read some paper in which it's demonstrated conclusively that dependent
types are irredeemably hopeless. Could somebody put me out of my misery
and drop me the reference?

Not that I'm at all miserable