A heterogenous list (difflist) that you can both append to and safely access elements

Learning
7

If you start with a concatenable heterogeneous list:

type ('list,'last) t =
  | []: ('a,'a) t
  |(::): 'a * ('l, 't) t -> ('a -> 'l, 't) t

let rec (@):
  type start mid last. (start,mid) t -> (mid,last) t -> (start,last) t =
  fun l r -> match l with
    | [] -> r
    | a :: q -> a :: (q @ r)

You can sort of get back a total head function by fixing the type of the tail

let split: (_,unit) t -> _ = function 
| a :: q  -> a, q 
| _ -> .

In your specific case, if you want to map and append to a different list, it seems to work fine at first

let l0 = [1;"one"]
let u = []

let x, l = split l
let u = u @ [x]

let y , l = split l
let u = u @ [ y^"'"]

In particular, u and l ends up with compatible types:

let diff = u <> l0

But unfortunately, when one looks closer, there is a lot of weak type variables due to the value restriction.
In particular, the type of u ends up being (int -> string -> '_weak1, '_weak1) t. Thus, it cannot be freely concatenated.

1 Like