About contracts and dependent types: of course full dependent types are undecidable, but those are rarely needed?  On 
the other hand, linear constraints over the integers are often needed, AND are not only fully decidable, there are 
both nice complexity results as well as practical algorithms [not both together :-( yet].

What puzzles me is that some decidable subset of dependent types is not part of any 'real' programming language (like 
Ocaml or Haskell).  

Certainly the Array code just posted is a nice example where having dependent types with only linear constraints over 
the integers as the 'extra' power is enough to resolve everything.  In fact, it seems that almost all examples of 
dependent types that I have seen in the type theory litterature are of this kind; counter-examples typically use 
polynomial constraints, which are undecidable in general.

Or am I missing something obvious that makes this much harder than it seems?

Jacques
  

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners