GATDs gone mild
(** Supporting code for the "GADTs gone mild" talk *) | |
(** Compact Arrays | |
https://blogs.janestreet.com/why-gadts-matter-for-performance/ | |
*) | |
module CompactArray = struct | |
type 'a t = | |
| Array of 'a array | |
| String of string | |
let get x i = match x with | |
| Array a -> Array.get a i | |
| String s -> String.get s i | |
end | |
(** Expressions without GADTs *) | |
module BoringExpr = struct | |
type expr = | |
| Int of int (* 42 *) | |
| Bool of bool (* true *) | |
| Add of expr*expr (* e + e *) | |
| If of expr*expr*expr (* if b then e else e*) | |
| Equal of expr*expr (* e = e *) | |
(* if 1 = 2 then 3 else 4 *) | |
let e = If (Equal (Int 1, Int 2), Int 3, Int 4) | |
type value = I of int | B of bool | |
let rec eval e = match e with | |
| Int i -> I i | |
| Bool b -> B b | |
| Add (e1,e2) -> | |
let v1 = eval e1 and v2 = eval e2 in | |
(match v1, v2 with | |
| I i1, I i2 -> I (i1 + i2) | |
| _ -> failwith "Moule a gaufres!") | |
| If (b, e1, e2) -> | |
(match eval b with | |
| B true -> eval e1 | |
| B false -> eval e2 | |
| I _ -> failwith "Anacoluthe!") | |
| Equal (e1, e2) -> | |
(match eval e2, eval e2 with | |
| I i1, I i2 -> B (i1 = i2) | |
| B b1, B b2 -> B (b1 = b2) | |
| _ -> failwith "Crétin des Alpes!") | |
end | |
(** Expressions with GADTs *) | |
module FancyExpr = struct | |
type 'a expr = | |
| Int: int -> int expr | |
| Bool: bool -> bool expr | |
| Add: int expr * int expr -> int expr | |
| If: bool expr * 'a expr * 'a expr -> 'a expr | |
| Equal: 'a expr * 'a expr -> bool expr | |
(* if 1 = 2 then 3 else 4 *) | |
let e = If (Equal (Int 1, Int 2), Int 3, Int 4) | |
let rec eval | |
: type a. a expr -> a | |
= fun e -> match e with | |
| Int i -> i | |
| Bool b -> b | |
| Add (e1,e2) -> | |
let v1 = eval e1 and v2 = eval e2 in | |
v1 + v2 | |
| If (b, e1, e2) -> | |
if eval b then eval e1 else eval e2 | |
| Equal (e1, e2) -> (eval e1 = eval e2) | |
let x : int = eval e | |
end | |
(** Miniformat and heterogenous lists. | |
http://drup.github.io/2016/08/02/difflists/ | |
*) | |
module HList = struct | |
type ('ty,'v) t = | |
| Nil : ('v, 'v) t | |
| Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t | |
let cons x l = Cons (x,l) | |
let plus1 l = Cons ((),l) | |
let one x = Cons (x,Nil) | |
let l1 = Cons (1, Cons ("bla", Nil)) | |
let l2 = Cons ((), Cons (2., Nil)) | |
let l3 = Cons (1, Cons ("bla", Cons ((), Cons(2.,Nil)))) | |
let rec append | |
: type a b c. | |
(a, b) t -> | |
(b, c) t -> | |
(a, c) t | |
= fun l1 l2 -> match l1 with | |
| Nil -> l2 | |
| Cons (h, t) -> Cons (h, append t l2) | |
end | |
module MiniFormat = struct | |
type ('ty,'v) t = | |
| End : ('v,'v) t | |
| Constant : string * ('ty,'v) t -> ('ty,'v) t | |
| Hole : ('ty, 'v) t -> (string -> 'ty, 'v) t ;; | |
let rec kprintf | |
: type ty res. (string -> res) -> (ty,res) t -> ty | |
= fun k -> function | |
| End -> k "" | |
| Constant (const, fmt) -> | |
kprintf (fun str -> k @@ const ^ str) fmt | |
| Hole fmt -> | |
let f s = kprintf (fun str -> k @@ s ^ str) fmt | |
in f ;; | |
let printf fmt = kprintf (fun x -> x) fmt ;; | |
(* "%s | %s" *) | |
let ex = Hole (Constant (" | ", Hole End)) ;; | |
printf ex "foo" "zoo" ;; | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment