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

[Goswin von Brederlow <goswin-v-b@web.de>]

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
 *)