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

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

[Goswin von Brederlow]

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

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

[Gabriel Scherer]

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.

GADTs are not as expressive as full dependent types and, I would
argue, their "intended use" is elsewhere. GADTs are plain old
algebraic datatypes that come with equality constraints between types.
By manipulating GADTs you can reason, in a convenient way, about some
types being equal to some other in specific case. The cornerstone
example of GADT is the (a) type of well-typed expressions (a  expr),
where the shape of the expression gives you more information about the
type (a) :

  type _ expr =
    | Int : int -> int expr
    | Prod : 'a expr -> 'b expr -> ('a * 'b) expr
    | IfThenElse : bool expr -> 'a expr -> 'a expr -> 'a expr
...

With a GADT type, you can write an evaluation function of type ('a
expr -> 'a), for instance, which would not be possible in a type-safe
way with the usual algebraic datatype with a phantom type parameter --
it was already possible to use encodings of GADT into first-class
modules [1], or finally tagless representations [2] to achieve the
same effect, but with more boilerplate and less efficient runtime
representations.

[1] http://okmij.org/ftp/ML/first-class-modules/
[2] http://okmij.org/ftp/tagless-final/index.html

(Remark: a lot of algorithms can be understood as the transformation
of data into code, that is evaluating a specific language of commands.
It is therefore easy to see "a type of well-typed expressions" in
almost every real-life use case.)

On the contrary, your intended applications are not directly about
equality between types, but about value and computations at the type
level. While this can be done with GADTs when extended with enough
machinery (in particular higher-kinded type variables and possibly
higher-kinded datatypes; see the work on Omega [3] for example), in
OCaml that is expected to be heavy, painful to write and read, and
hard on the tooling (type inference, error messages, etc.). At some
point the benefit of finer static checking does not compensate the
overall pain and complexity of the whole process, and I think we enter
the realm of unnecessarily complicated programs.

[3] http://web.cecs.pdx.edu/~sheard/

I'm no expert on the subject, but I doubt GADT will provide you much
more expressivity at the level of which computation you can embed in
types. I suspect you'll mostly use the same techniques as you used
before with phantom types (the question of signature redundancy being
more a technical detail than an indication of expressivity, or lack
thereof, of one or another technique). Unary natural numbers will keep
being easy to express at the type-level (see draft implementation at
the end of this email), and modulo, difference or what not will
probably stay tricky and horrible to define if you want the
*inference* engine to do all computation. There is also this technique
of using term witnesses to do the heavy type lifting and use a
logic-programming style at the type level, but that's probably not
what you're looking for.

A small draft of unary natural numbers mirrored at the type level through GADT.
  https://gitorious.org/gasche-snippets/ocaml-typed-units/blobs/master/gadts_and_type_level_numbers.ml

They quickly get painful and impractical. Implementing addition is
already non-trivial -- see Mandelbaum and Stump's 2009 article "GADTs
for the OCaml masses" [4] for a more featureful, but no simpler,
presentation:

[4] https://www.cs.uiowa.edu/~astump/papers/icfp09.pdf

I consider using GADT to emulate dependent types to be an advanced,
and often counter-productive, level of "type hackery". We should
rather seek examples that fit the GADT features well, instead of
trying to stretch it to such unreasonable places. For example,
François Pottier and Nadji Gauthier's "Polymorphic typed
defunctionalization and concretization" article [5] (2004, 2006) uses
GADT to represent functions by (well-typed) data tags, and Alain
Frisch's use of GADTs for dynamic type witnesses [6]. But with such
advanced features, it is of course not easy to draw a line between
"reasonable" and "less reasonable" uses.

[5] http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf
[6] http://www.lexifi.com/blog/dynamic-types




On Mon, Mar 12, 2012 at 12:30 PM, Goswin von Brederlow
<goswin-v-b@web.de> wrote:
> 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
>  *)
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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

[Jesper Louis Andersen]

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.

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

[Raoul Duke]

On Mon, Mar 19, 2012 at 9:13 AM, Jesper Louis Andersen
> If you want to play with dependent types, there are two ways which
> seem popular at the moment: Agda or Coq.

and some not popular ones...

http://www.ats-lang.org/

http://sandycat.info/blog/deptypes-shen/

et. al.

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

[Goswin von Brederlow]

Raoul Duke <raould@gmail.com> writes:

> On Mon, Mar 19, 2012 at 9:13 AM, Jesper Louis Andersen
>> If you want to play with dependent types, there are two ways which
>> seem popular at the moment: Agda or Coq.
>
> and some not popular ones...
>
> http://www.ats-lang.org/
>
> http://sandycat.info/blog/deptypes-shen/
>
> et. al.

Neigther of which are examples for GADT in ocaml.

MfG
        Goswin

[Caml-list] GADT example for universal list

[Goswin von Brederlow]

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 = <fun>
val print : list -> unit = <fun>
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 = <fun>

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

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

[Gabriel Scherer]

In this example, you use GADTs to safely provide runtime type
information on untagged data. This can also be seen as a specific case
of the "runtime type information" promoted by Alain Frisch [1] or
equivalently as a dual (in the sum-of-data vs. product-of-functions
sense) of type-classes, where you have a predicate over a subset of
the types ("sif" being read as an "is_a_number" type constraint) whose
instances are closed / fixed at class definition time, to which
operations can be added modularly: `add` now, `mult` later. This can
then be related to Pottier and Gauthier's "concretization" of
type-classes mentioned in my previous message.

[1] http://www.lexifi.com/blog/dynamic-types
[2] http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf

> One can write typed interpreters in the
> final-tagless style, with no GADTs.

Isn't this true of all GADTs examples? You have already shown that
GADTs can be relatively-practically expressible with equality types. I
suspect the justification for GADTs is not increased expressivity, but
a simpler/more familiar way to implement those
type-information-passing techniques -- just as ordinary algebraic
datatypes could be expressed with functional encodings, but are more
practical and convenient to use in the usual case. Besides, there is
the down-to-earth efficiency benefit of directly using first-order
data instead of functional encodings.

On Thu, Mar 22, 2012 at 7:01 AM,  <oleg@okmij.org> wrote:
>
> Somehow typed tagless interpreters (embeddings of a typed language)
> and length-parameterized lists with the append function are the most
> popular examples of GADTs. Neither of them seem to be particularly
> good or compelling examples. One can write typed interpreters in the
> final-tagless style, with no GADTs. Writing append function whose type
> says the length of the resulting list is the sum of the lengths of the
> argument lists is cute. However, this example does not go too far, as
> one discovers when trying to write List.filter for
> length-parameterized lists.
>
> The ML2010 talk on GADT emulation specifically used a different
> illustrating example: a sort of generic programming, or implementing
> N-morphic functions:
>  http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf
>
> Polymorphic functions must operate uniformly on their arguments, which
> means they can't use a specific efficient operation if the argument
> happens to be of a convenient type (like int of float
> array). N-morphic functions can take such an advantage.
>
> The running example of the talk combined value and the shape
> information in the same data type:
>
> type 'a sif = Int of (int,'a) eq * int
>            | Flo of (float,'a) eq * float
>
> val add_sif : 'a sif ->  'a sif -> 'a sif
>
> Shape may well be separated from the value:
>
> type 'a shape = Int of (int,'a) eq
>              | Flo of (float,'a) eq
>
> val add_sif : 'a shape -> 'a -> 'a -> 'a
>
> and so we pass values to add_sif without `boxing' and wrapping.
>
>
>
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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

[oleg]

Somehow typed tagless interpreters (embeddings of a typed language)
and length-parameterized lists with the append function are the most
popular examples of GADTs. Neither of them seem to be particularly
good or compelling examples. One can write typed interpreters in the
final-tagless style, with no GADTs. Writing append function whose type
says the length of the resulting list is the sum of the lengths of the
argument lists is cute. However, this example does not go too far, as
one discovers when trying to write List.filter for
length-parameterized lists.

The ML2010 talk on GADT emulation specifically used a different
illustrating example: a sort of generic programming, or implementing
N-morphic functions:
 http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf

Polymorphic functions must operate uniformly on their arguments, which
means they can't use a specific efficient operation if the argument
happens to be of a convenient type (like int of float
array). N-morphic functions can take such an advantage.

The running example of the talk combined value and the shape
information in the same data type:

type 'a sif = Int of (int,'a) eq * int
            | Flo of (float,'a) eq * float

val add_sif : 'a sif ->  'a sif -> 'a sif

Shape may well be separated from the value:

type 'a shape = Int of (int,'a) eq
              | Flo of (float,'a) eq 

val add_sif : 'a shape -> 'a -> 'a -> 'a

and so we pass values to add_sif without `boxing' and wrapping.