From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2JGDsFL003601 for ; Mon, 19 Mar 2012 17:13:54 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Au4BAPJSZ0/RVaC0kGdsb2JhbABChT6xBAgiAQEBAQkJDQcUBCOCCQEBAQMBEgIPHQEbHQEDAQsGBQsPAiYCAiEBAREBBQEcBhMZCYdjBZx4CotEToJxhHA/iHQBBQuBJIgmhhGBFgSVaIsvgxo9hAk X-IronPort-AV: E=Sophos;i="4.73,611,1325458800"; d="scan'208";a="136782592" Received: from mail-gy0-f180.google.com ([209.85.160.180]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Mar 2012 17:13:48 +0100 Received: by ghbz12 with SMTP id z12so8194208ghb.39 for ; Mon, 19 Mar 2012 09:13:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=1Vy4d2U5qWtqfso1l6+3Mjt8ed/ON2wbqz7eS/0fkd0=; b=tbSS66tonF55coTK3Hxwayf31SMg1D7rIkTm/Yo9m/uG0KKzaJut/Ye2K27hxjqLtO YdOlqhfnaNBBpAttS60P8LJCwAyv12CFCZFVKCl/Vu5oZe3sIdQ0xCE1Appi4gEZzfZ5 cw2vhXxs6AFF+x3fUUyB1yGdFcvGcdAgIVb8S9mkGYSXqe5Y/PdSapuhabDqS9tDbpiU d6sFca4VjH77AEWYBCIyEhQg7a3s443ccmwfPNVI8Ucle5VFiX0V6YMzQzr63AuSxEdC V6gpyTO5nQmlmh+FEhqVcfq/+N/TPsB1uh5Pc+MEOAYaB/AYYfMzkMeYYQXHRPcezQpw 9xow== Received: by 10.60.13.132 with SMTP id h4mr14179931oec.62.1332173626747; Mon, 19 Mar 2012 09:13:46 -0700 (PDT) MIME-Version: 1.0 Received: by 10.182.127.98 with HTTP; Mon, 19 Mar 2012 09:13:26 -0700 (PDT) In-Reply-To: References: <87aa3mawg1.fsf@frosties.localnet> From: Jesper Louis Andersen Date: Mon, 19 Mar 2012 17:13:26 +0100 Message-ID: To: Gabriel Scherer Cc: Goswin von Brederlow , caml-list@yquem.inria.fr Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Wanted: GADT examples: string length, counting module x On Mon, Mar 19, 2012 at 15:43, Gabriel Scherer 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.