OCaml how to implement swap on a heterogeneous list?

geckos 0
Viewed 73

I was following this tutorial https://drup.github.io/2016/08/02/difflists/

And tried to implement a swap on a heterogeneous list, but it doesn't typecheck

type ('ty, 'v) t =
  | Nil : ('v, 'v) t
  | Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t

let plus1 l = Cons ((), l) (* : ('a, 'b) t -> (unit -> 'a, 'b) t *)
let one x = Cons (x, Nil) (* : 'a -> ('a -> 'b, 'b) t *)
let l1 = Cons (1, Cons ("bla", Nil)) (* : (int -> string -> 'a, 'a) t *)
let l2 = Cons ((), Cons (true, Nil)) (*: (unit -> float -> 'a, 'a) t *)
let l3 = Cons (1, Cons ("bla", Cons ((), Cons (true, Nil)))) (*: (int -> string -> unit -> float -> 'a, 'a) t *)

let rec append
  : type ty1 ty2 v.
    (ty1, ty2) t ->
    (ty2, v) t ->
    (ty1, v) t =
  fun l1 l2 -> match l1 with
  | Nil -> l2
  | Cons (h, t) -> Cons (h, append t l2)

let l4 = Cons (1, Cons ("bla", Nil)) (* : (int -> string -> 'a, 'a) t *)
let l5 = Cons ("bla", Cons (1, Nil)) (* : (string -> int -> 'a, 'a) t *)

let swap
  : type ty1 ty2 v. 
  (ty1 -> ty2 -> v, v) t ->
  (ty2 -> ty1 -> v, v) t =
  function
  | Nil -> Nil
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
  | Cons (a, Nil) -> Cons (a, Nil)

I get

Error: This expression has type (ty2 -> ty1 -> v, ty2 -> ty1 -> v) t
       but an expression was expected of type (ty2 -> ty1 -> v, v) t
       Type ty2 -> ty1 -> v is not compatible with type v

In the | Nil -> Nil line, I understand that the types do not match but don't know where to go from here

If I try

let swap
  : type ty1 ty2 v. 
  (ty1 -> ty2 -> v, v) t ->
  (ty2 -> ty1 -> v, v) t =
  function
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))

I get this warning

File "./difflist.ml", lines 27-28, characters 2-52:
27 | ..function
28 |   | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Cons (_, Nil)

The same for Nil, I can do this though, but seems not ideal

let swap
  : type ty1 ty2 v. 
  (ty1 -> ty2 -> v, v) t ->
  (ty2 -> ty1 -> v, v) t =
  function
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
  | Cons (_, Nil) -> assert false
  | Nil -> assert false

I can't call it will a list smaller than 2 which is expected. I expect that since the typechecker can detect ill-typed calls it would not complain about the match not being exhaustive

If I try the matches with assert false I got these errors (which are expected)

let l7 = swap Nil
(* This expression has type ('a -> 'b -> 'c, 'a -> 'b -> 'c) t
but an expression was expected of type ('a -> 'b -> 'c, 'c) t
The type variable 'd occurs inside 'e -> 'f -> 'd *)
let l8 = swap (Cons (true, Nil))
(* This expression has type ('a -> 'b, 'a -> 'b) t
but an expression was expected of type ('a -> 'b, 'b) t
The type variable 'c occurs inside 'd -> 'c *)

Is there any way to get rid of these assert false?

ocaml
1 Answers

The issue is that the swap function is only defined for list of length greater than two, and the difflist heterogeneous lists do not encode length at the type level. Indeed, a list of type (ty->ty2->mid,last) t could have any lengths. For instance,

let t: (int -> float -> int, int -> float -> int) t = Nil

is valid.

One option is thus to return an option type like for an homogeneous list and return None if the list length is too small:

let swap
  : type ty1 ty2 v tl.
  (ty1 -> ty2 -> v, tl) t ->
  (ty2 -> ty1 -> v, tl) t option =
  function
  | Nil -> None
  | Cons(_,Nil) -> None
  | Cons (a, Cons (b, tl)) -> Some(Cons (b, Cons (a, tl)))

Another option is to close the list to further extension by fixing the type of the tail:

type void = |
let swap
  : type ty1 ty2 tl.
  (ty1 -> ty2 -> tl, void) t ->
  (ty2 -> ty1 -> tl, void) t =
  function
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
  | _  -> .
  | Cons(_,_) -> .

Here I am using an empty type for the type of the tail because this type is no linked to the type of any value but any other ground type would work.

octachron0
Related