From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2CBUkpf002144 for ; Mon, 12 Mar 2012 12:30:46 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjsDAJPdXU/ZSMDzjmdsb2JhbABBtVgiAQEBAQkLCQkSBSSCNxN7NAEEKIhCnlaYBpEBBJsijTE X-IronPort-AV: E=Sophos;i="4.73,570,1325458800"; d="scan'208";a="148824944" Received: from fmmailgate05.web.de ([217.72.192.243]) by mail1-smtp-roc.national.inria.fr with ESMTP; 12 Mar 2012 12:30:41 +0100 Received: from moweb001.kundenserver.de (moweb001.kundenserver.de [172.19.20.114]) by fmmailgate05.web.de (Postfix) with ESMTP id A39F66B3B193 for ; Mon, 12 Mar 2012 12:30:35 +0100 (CET) Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb001) with ESMTPA (Nemesis) id 0LkPW7-1SeBHk31Zb-00cENG; Mon, 12 Mar 2012 12:30:28 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.77) (envelope-from ) id 1S73S2-00075e-Gy for caml-list@yquem.inria.fr; Mon, 12 Mar 2012 12:30:06 +0100 From: Goswin von Brederlow To: caml-list@yquem.inria.fr Date: Mon, 12 Mar 2012 12:30:06 +0100 Message-ID: <87aa3mawg1.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:yBVCVE0bN6nBfaTuP51NlhJmwjKoKIyq4r6go6UpwiK vi/URYVHjLVWgrYfpmOp7iz8Zn0LI8CY0XSmV5off3YDXg26ud l2XwN/9nnWype7zlo5zi4HvGX+EA2wcHs2UvTfTsfpeVD7S9NZ sC413cggjqUeu4SMt0Tn4GtGjpGavOj3sECv6KzO0pVYKbt09N ZXhihOMwEt9/Ne1gmZaYg== Subject: [Caml-list] Wanted: GADT examples: string length, counting module x Hi, yesterday I compiled ocaml 3.13 and played around a bit with the GDAT syntax but wasn't overly successfull. Or at least I had higher hopes for it. So it is time to invoke the internet to come up with a better example. :) 1) How do I write a GADT that encodes the length of a string or array? How do I use that to create a string or array? How do I specify a function that takes a string or array of a fixed length? Bonus: How do I specify a function that takes a string or array of a certain length or longer? 2) How do I write a GADT that counts an int module x? Say for an offset into a byte stream to safeguard when access is aligned and when unaligned. Again with an example that creates a value and a function that uses it. Bonus: Have one function that only allows aligned access and one that picks the right aligned/unaligned function to use depending on the type. Below I've included an example for checking aligned access (1/2/4/8 byte aligned). First using GADT and second using old style phantom types. The second looks much longer because it includes the signature needed to make the type (...) off private. The t1/t2/t4/t8 types are just aliases to make the type of the other functions shorter. One thing I couldn't manage is to write a "bind" function with GADTs or bind takeX to a string unless I specify the full type. "takeX s" always switches to '_a types and then gets bound to a specific type on the first use and fail on the second use. On the plus side of GADTs is that you do not need a private type (and therefore the module signature) to make them work. MfG Goswin PS: Other simple examples that show the power of GADTs are welcome too. ---------------------------------------------------------------------- (* Declare GADT type *) type z type u type _ t = | Zero : ((z * u) * (z * u * u * u) * (z * u * u * u * u * u * u * u)) t | Succ : (('a * 'b) * ('c * 'd * 'e * 'f) * ('g * 'h * 'i * 'j * 'k * 'l * 'm * 'n)) t -> (('b * 'a) * ('d * 'e * 'f * 'c) * ('h * 'i * 'j * 'k * 'l * 'm * 'n * 'g)) t (* start of stream *) let zero = (Zero, 0) (* advance by 1, 2, 4 or 8 *) let succ1 x = Succ x let succ2 x = succ1 (succ1 x) let succ4 x = succ2 (succ2 x) let succ8 x = x (* take 1, 2, 4 or 8 bytes with alignment restriction *) let take1 : type a b c d e f g h i j k l m n. string -> (((a * b) * (c * d * e * f) * (g * h * i * j * k * l * m * n)) t * int) -> ((((b * a) * (d * e * f * c) * (h * i * j * k * l * m * n * g)) t * int) * string) = fun s (t, x) -> ((succ1 t, x+1), String.sub s x 1) let take2 : type c d e f g h i j k l m n. string -> (((z * u) * (c * d * e * f) * (g * h * i * j * k * l * m * n)) t * int) -> ((((z * u) * (e * f * c * d) * (i * j * k * l * m * n * g * h)) t * int) * string) = fun s (t, x) -> ((succ2 t, x +2), String.sub s x 2) let take4 : type g h i j k l m n. string -> (((z * u) * (z * u * u * u) * (g * h * i * j * k * l * m * n)) t * int) -> ((((z * u) * (z * u * u * u) * (k * l * m * n * g * h * i * j)) t * int) * string) = fun s (t, x) -> ((succ4 t, x+4), Str ing.sub s x 4) let take8 : string -> (((z * u) * (z * u * u * u) * (z * u * u * u * u * u * u * u)) t * int) -> ((((z * u) * (z * u * u * u) * (z * u * u * u * u * u * u * u)) t * int) * string) = fun s (t, x) -> ((succ8 t, x+8), String.sub s x 8) (* Test string *) let s = "aabbccccdddddddd" (* extract things from string *) let foo () = let (off, a) = take1 s zero in let (off, b) = take1 s off in let (off, c) = take2 s off in let (off, d) = take4 s off in let (off, e) = take8 s off in Printf.printf "%s %s %s %s %s\n" a b c d e (* using take2/4/8 with an offset that isn't aligned gives a compile time type error: let bad () = let (off, a) = take1 s zero in take8 s off *) ---------------------------------------------------------------------- module M : sig (* Types for aligned unaligned tracking *) type z type u (* The type of an offset into a stream *) type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off = private int (* Start of the stream *) val zero : (z, u, z, u, u, u, z, u, u, u, u, u, u, u) off (* Coercion to integer, same as (x :> int) *) val get : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> int (* Advance the position by 1, 2, 4 or 8 *) val succ : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ('b , 'a, 'd, 'e, 'f, 'c, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'g) off val succ2 : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ('a , 'b, 'e, 'f, 'c, 'd, 'i, 'j, 'k, 'l, 'm, 'n, 'g, 'h) off val succ4 : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ('a , 'b, 'c, 'd, 'e, 'f, 'k, 'l, 'm, 'n, 'g, 'h, 'i, 'j) off val succ8 : ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ('a , 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off (* Aliases for shorter type names *) type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t1 = ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> (('b, 'a, 'd, 'e, 'f, 'c, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'g) off * string) type ('c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t2 = (z, u, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ((z, u, 'e, 'f, 'c, 'd, 'i, 'j, 'k, 'l, 'm, 'n, 'g, 'h) off * string) type ('g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t4 = (z, u, z, u, u, u, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ((z, u, z, u, u, u, 'k, 'l, 'm, 'n, 'g, 'h, 'i, 'j) off * string) type t8 = (z, u, z, u, u, u, z, u, u, u, u, u, u, u) off -> ((z, u, z, u, u, u, z, u, u, u, u, u, u, u) off * string) (* Take 1, 2, 4 or 8 byte with alignment restriction *) val take1 : string -> ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t1 val take2 : string -> ('c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t2 val take4 : string -> ('g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t4 val take8 : string -> t8 (* Bind all take functions to a string for easier use *) val bind : string -> (('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t1 * ('c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t2 * ('g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t4 * t8) end = struct (* Types for aligned unaligned tracking *) type z type u (* The type of an offset into a stream *) type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off = int (* Start of the stream *) let zero = 0 (* Coercion to integer, same as (x :> int) *) let get x = x (* Advance the position by 1, 2, 4 or 8 *) let succ x = x + 1 let succ2 x = succ (succ x) let succ4 x = succ2 (succ2 x) let succ8 x = succ4 (succ4 x) (* Aliases for shorter type names *) type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t1 = ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> (('b, 'a, 'd, 'e, 'f, 'c, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'g) off * string) type ('c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t2 = (z, u, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ((z, u, 'e, 'f, 'c, 'd, 'i, 'j, 'k, 'l, 'm, 'n, 'g, 'h) off * string) type ('g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) t4 = (z, u, z, u, u, u, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n) off -> ((z, u, z, u, u, u, 'k, 'l, 'm, 'n, 'g, 'h, 'i, 'j) off * string) type t8 = (z, u, z, u, u, u, z, u, u, u, u, u, u, u) off -> ((z, u, z, u, u, u, z, u, u, u, u, u, u, u) off * string) (* Take 1, 2, 4 or 8 byte with alignment restriction *) let take1 = fun s x -> (succ x, String.sub s (get x) 1);; let take2 = fun s x -> (succ2 x, String.sub s (get x) 2);; let take4 = fun s x -> (succ4 x, String.sub s (get x) 4);; let take8 = fun s x -> (succ8 x, String.sub s (get x) 8);; (* Bind all take functions to a string for easier use *) let bind s = (take1 s, take2 s, take4 s, take8 s) end open M (* Test string *) let s = "aabbccccdddddddd" let (t1, t2, t4, t8) = bind s (* extract things from string *) let foo () = let (off, a) = t1 zero in let (off, b) = t1 off in let (off, c) = t2 off in let (off, d) = t4 off in let (off, e) = t8 off in Printf.printf "%s %s %s %s %s\n" a b c d e (* using take2/4/8 with an offset that isn't aligned gives a compile time type error: let bad () = let (off, a) = take1 s zero in take8 s off *)