hlist_index.ml

(* empty type*)
type void = private Void

(* list type *)
type _ hlist =
  | Nil: void hlist
  | Cons:
      'elt * 'a hlist -> ( 'elt * 'a ) hlist

let rec length: type a. a hlist -> int = function%with_ll
  | [] -> 0
  | _::q -> 1 + length q

type (_,_) index =
  | Z: ('a * 'any, 'a) index
  | S: ('a,'b) index -> ('any * 'a, 'b) index

let rec get: type elts return. elts hlist -> (elts, return) index -> return =
  fun l index -> match l, index with
    | Cons(a, _) , Z -> a
    | Cons(_,q), S n -> get q n
    | Nil, _ -> .