List with GADTs

Learning
1

Hi,

I am learning GADTs and found the below snippet at ocamlgadt. I find that using GADTs, OCaml can check if a list passed to a function is empty or not at compile time!

I have an issue with the snippet though - the list is heterogeneous.
How could i make it homogeneous without breaking hd function?

Thanks.

module GList = struct 
    type zero
    and _ t =
        | [] :  zero t
        | ( :: ) : 'a * 'b t -> ('a * 'b) t
    
    let hd : type a. (a * _) t -> a = function (h :: _) -> h ;;   
end ;;

GList.hd (["hello"; 1.1; 1; 'a']: (_ * _) GList.t) ;;
GList.hd ([] : (_ * _) GList.t) ;;
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