List with GADTs

Learning
2

There are lots of different ways to do it. Here is a possibility. It changes the type family t so that its first argument is the type of the list elements and the second one is a type-level boolean that indicates whether the list has elements:

type (_, _) t =
    | [] :  ('a, float) t
    | ( :: ) : 'a * ('a, 'b) t -> ('a, unit) t

let hd : type a. (a, unit) t -> a = function (h :: _) -> h
4 Likes