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

#1

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.

(experiments here: https://gist.github.com/wokalski/8f765caf542158a87fcf13b88fe577a5#file-experiments-re)

#2

Here’s a useful article about implementing diff lists using GADTs (note: the syntax is in OCaml, but it should translate to Reason).

#3

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 *)
#4

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

A good tutorial is the lesson of @yallop here.

#5

Thanks! I’ll have a look at the lesson.

@dinosaure when it comes to your snippet, it does work for homogenous lists nicely but when I try to make such list heterogenous, it gets problematic:

https://sketch.sh/s/jsJd7q0NAbkkRrN3IhJ8Ca/

I have tried several such implementations but at the end the problem was always the same, how to go from t1 -> t2 -> 'a to t1 -> t2 -> t3 -> 'a

Sorry if I’m not being clear here. I feel like I lack vocabulary to communicate this clearly.

#6

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)
#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
#8

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.

#9

Thank you @octachron (yet another time :slight_smile:.) I managed to implement a list with the desired properties thanks to the suggestion to fix the type of tail.

Thanks to all of you for the help. Much appreciated!

#10

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

also available in sketch here:
https://sketch.sh/s/jsJd7q0NAbkkRrN3IhJ8Ca/

1 Like