Hi 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 Conor