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.