Re: [Caml-list] Depend-type beginner question

[Arnaud Spiwack <aspiwack@lix.polytechnique.fr>]

>
> Of course. So languages that claim to have dependant types all delay 
> the type checking to compile-time or formal proof. I am reassured, I 
> thought I was missing some big thing... 
I'm not sure I'm quite getting what you mean here.
 In any case, dependent types mainly means that there is a bit of 
computation inside types. This raises quite a lot of issues.
 It is way preferable, for instance, that type-checking is decidable, 
which means that one can't put arbitrary computation inside types, 
moreover, it would be preferable that a type does not read or write into 
files, that would be rather annoying.
In order to get things done, there are a few approachs, languages like 
OCaml, Haskell, and such, try to build up from decidable inference to 
richer type systems and see what they can get done, this have the 
advantages of manipulating fully usable languages; languages like Coq, 
Agda, Epigram, start with dependent types as highly expressive as 
possible, and try to retrieve features bit by bit (and thus are not 
fully usable languages). (I haven't quoted DML and PML because I still 
haven't quite looked into them, thus I can't really place them :p ).

However, to get back to the list example.
Let us suppose, in Coq syntax, that we defined lists the following way :

Inductive list (A:Type) : nat -> Type :=
   | Nil : forall A, list A 0
   | Cons : forall A n, A -> list A n -> list A (S n)

These are lists that carry their length.

The program :

if b then
  []
else
  [a]

can only be typed as a *dependent* elimination of b, as Christophe said 
the type is "if b then list A 0 else list A 1". The whole point of 
dependent types is that this is a perfectly well-formed type. And it can 
be checked before compiling "if b then [] else [a]" that it actually 
have type "if b then list A 0 else list A 1". The schyzophrenia of 
dependent types, is that types depend on previously compiled (and types) 
expressions, it still is static typing, just weirder (and much more fun 
if you want my opinion ;) ).


Arnaud Spiwack