On Mon, Mar 19, 2012 at 15:43, Gabriel Scherer <gabriel.sche...@gmail.com> wrote:
> I suspect you're seeing too much into the GADT as they're being added > in OCaml. Your examples are not basically about GADTs, but about > dependent types: you want to encode values (and operations on them) at > the type level to get more expressivity. This is a well-known and > extremely powerful trend in programming languages design, but it also > results in complex systems with sophisticated rules. I like the view of Conor McBride: the types are Priests overseeing the terms which are people. In a language like OCaml the priests and people and not allowed to mingle with each other. What is in the church of types, stays in the church of types. This means - and I believe this is what the remainder of Gabriels post is about - that the priests need to encode the people or that you need to represent the terms as a mirroring in the types. Real dependent types allow the priests and people to intermingle in a specific way: terms can be part of types. Or more succinctly: Types can be indexed by terms. This construction allow you to take a term from the language, say n : nat, and then talk about the type 'vector n', i.e., the vector (list) of length n. If you want to play with dependent types, there are two ways which seem popular at the moment: Agda or Coq. Agda is the more experimental and programming-language-like path, whereas Coq is a full proof assistant with automation support. But others live their life in these tools much more than I, and they would be more knowledgable in what to use. -- J. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
