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 q2N17np3028026 for ; Fri, 23 Mar 2012 02:07:49 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnkCAHXMa0/ZSMDzk2dsb2JhbABEt0MiAQEBAQkJCwkUAySCCgEFJxNPLBQRDwEEKIhCuCGNQoMiBJs6jTU X-IronPort-AV: E=Sophos;i="4.73,633,1325458800"; d="scan'208";a="137348698" Received: from fmmailgate05.web.de ([217.72.192.243]) by mail4-smtp-sop.national.inria.fr with ESMTP; 23 Mar 2012 02:07:48 +0100 Received: from moweb002.kundenserver.de (moweb002.kundenserver.de [172.19.20.108]) by fmmailgate05.web.de (Postfix) with ESMTP id 05FF66BB3150 for ; Fri, 23 Mar 2012 02:07:48 +0100 (CET) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb001) with ESMTPA (Nemesis) id 0MJTHn-1S7r6u35Gl-003AJ1; Fri, 23 Mar 2012 02:07:47 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1SAsyp-0003qR-6k for caml-list@yquem.inria.fr; Fri, 23 Mar 2012 02:07:47 +0100 From: Goswin von Brederlow To: caml-list@yquem.inria.fr References: <87aa3mawg1.fsf@frosties.localnet> Date: Fri, 23 Mar 2012 02:07:47 +0100 In-Reply-To: <87aa3mawg1.fsf@frosties.localnet> (Goswin von Brederlow's message of "Mon, 12 Mar 2012 12:30:06 +0100") Message-ID: <87k42ci0po.fsf@frosties.localnet> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Provags-ID: V02:K0:kYY9NlzeIGf0ajc0hKHd3pAtHy8q28ydh0gir7i2pq2 oxAOuzh8GM1bLe+S4i5r85XFa3FAQE6o26IUW0hANJTsvMoFUq rZIAC2I1jWkjN9Tf947WJ715OkeIDfLRBRHswh1x5mqm1P+J4f 0VoOE+lL4hY6P2bUqO3tn9+Y1IN1uNj9m+QeXx04Zxa3Vwi0fR B8Aifj5NialaQOUc0okcg== Subject: [Caml-list] GADT example for universal list Hi, I played some more with GADTs, this time with an universal list. Well, not truely universal as you can't store arbitrary types. Only Int and Float are allowed here: type _ kind = (* used for searching in the list *) | Int_kind : int kind | Float_kind : float kind type value = (* box the values so we have runtime type information *) | Int of int | Float of float type list = (* the universal list *) | Nil : list | Cons : value * list -> list (* find the first value in the list of a given kind *) let rec get : type a . list -> a kind -> a = fun l k -> match (k, l) with | (_, Nil) -> raise Not_found | (Int_kind, Cons (Int x, xs)) -> x | (Float_kind, Cons (Float x, xs)) -> x | (_, Cons (_, xs)) -> get xs k (* print out list *) let rec print = function | Nil -> print_newline () | Cons ((Int x), xs) -> Printf.printf "%d " x; print xs | Cons ((Float x), xs) -> Printf.printf "%f " x; print xs (* testing *) let empty = Nil let l1 = Cons ((Int 1), empty) let l2 = Cons ((Float 2.), l1) let () = print l2 let i = get l2 Int_kind let f = get l2 Float_kind;; (* 2.000000 1 type _ kind = Int_kind : int kind | Float_kind : float kind type value = Int of int | Float of float type list = Nil : list | Cons : value * list -> list val get : list -> 'a kind -> 'a = val print : list -> unit = val empty : list = Nil val l1 : list = Cons (Int 1, Nil) val l2 : list = Cons (Float 2., Cons (Int 1, Nil)) val i : int = 1 val f : float = 2. *) At first glance you might think: Why does that need GADTs? Why not simply use type value = Int of int | Float of float for this? Take a close look at the get funktion: val get : list -> 'a kind -> 'a = It does not return a value but directly the unboxed type. Because the value is unboxed you can directly use it and ocaml will detect if you screw up the type like in: let () = Printf.printf "%d\n" (get l2 Float_kind);; Error: This expression has type float but an expression was expected of type int MfG Goswin