Re: [Caml-list] Wanted: GADT examples: string length, counting module x

[Jesper Louis Andersen <jesper.louis.andersen@gmail.com>]

On Mon, Mar 19, 2012 at 15:43, Gabriel Scherer
<gabriel.scherer@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.