I would like to drop an element from one difflist, process it, and append to another heterogenous list. After N steps where N is the length of a list, I’d like to end up with a list of the same type as the list I started with. So I would like to do:
let l = Cons 1 Cons('a', Nil);
let l' = Nil
let (head, tail) = dropoFirst f
let l' = append l' (head + 1)
let (head, _) = dropoFirst tail
let l' = append l' head```
I’ve tried to make it work but I’m failing to create a list for which it’s both possible get the first element (knowing it does exist, without option) and append to the end of it.
I am aware of the article and correct me if I’m wrong but the difflist described there doesn’t have the desired properties. I.e. it’s not possible to safely get the head of the list when the list is non-empty. So:
let l = Cons 1 Nil;
let a, tail = head l (* a should be non-optional int *)
let a', _ = head tail (* This should cause a type error but it can't in that implementation *)
About that, you just need to put a witness of the length of your list like:
type z = Z : z
type 'x s = S : 'x -> 'x s
type ('a, 'l) list =
| [] : ('a, z) list
| (::) : 'a * ('a, 'l) list -> ('a, 'l s) list
let head : type a l. (a, l s) list -> a = function
| x :: _ -> x
If you want heterogeneous list with the possibility to retrieve its elements, you should use GADT as in this example:
type ('hd, 'tl) hlist =
| Nil : ('hd, 'tl) hlist
| Cons : 'hd, ('tl, 'a) hlist -> ('hd, 'tl * 'a) hlist
let drop_first : type a b c. (a , b * c) hlist -> a * (b, c) hlist = function
| Nil -> failwith "empty hlist"
| Cons (hd, tl) -> (hd, tl)
And if you want a type error (instead of exception) in case of empty list, you should mix this with @dinosaure trick:
type z = Z : z
type 'n s = S : 'n -> 'n s
type ('hd, 'tl, 'length) hlist =
| Nil : ('hd, 'tl, z) hlist
| Cons : 'hd * ('a , 'b, 'l) hlist -> ('hd, 'a * 'b, 'l s) hlist
let drop_first : type a b c. (a, b * c, 'n s) hlist -> a * (b, c, 'n) hlist =
fun (Cons (hd, tl)) -> (hd, tl)
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.
If you want to process elements of heterogeneous lists, you might also need some support for higher-kinded polymorphism (e.g. map a list with a function of type ('a, 'b) result -> 'a option, in general this is ('a, 'b) T1.t -> 'a T2.t). But higher-kinded polymorphism is not directly supported in OCaml. I once tried to implement some basic functions for higher-kinded heterogenious lists based on defunctionalization as described here. I made an example based on those attempts here.
I’ve found another interesting technique which allows us to use diff lists so that it’s possible to append to them in constant time and safely access elements:
type nil = | Nil
type 'list t =
| []: nil t
| (::) : 'a * 'l t -> ('a -> 'l) t
let init a = a
let append value x hole = x (value::hole)
let seal x = x []
let dropFirst =
function
| a::q -> a, q
let x = init |> append(2) |> append(2.) |> append("2") |> seal
let (_: int), x = dropFirst x
let (_: float), x = dropFirst x
let (_: string), x = dropFirst x
let y = init |> append(2.) |> append(2) |> seal
let (_: float), y = dropFirst y
let (_: int), y = dropFirst y
.) I managed to implement a list with the desired properties thanks to the suggestion to fix the type of tail.