Puzzle: Reverse a heterogeneous list twice

Hello,

Perhaps some of you might be interested in a little GADT puzzle… hopefullly it’s neither too hard nor too easy! The heterogeneous list is among the first examples of GADTs one learns about:

type nil = NIL

type _ hlist =
  | Nil  :                          nil hlist
  | Cons : 'x * 'xs hlist -> ('x * 'xs) hlist

This let us construct lists where elements can have different types: Cons (42, Cons ("hi", Cons ('z', Nil))) and the typesystem tracks each value type and the shape of the list: (int * (string * (char * nil))) hlist. But you can’t actually do much if you are only given an hlist since the types are not available at runtime (so you need additional machinery/assumptions to make an hlist useful in general).

One operation we can do though is to reverse an hlist (just like List.rev does). On the previous example, this would return:

Cons ('z', Cons ("hi", Cons (42, Nil)))
  :  (char * (string * (int * nil))) hlist
  1. If you are not too familiar with GADTs, then the first puzzle is to type the rev function, since val rev : 'xs hlist -> ??? hlist is going to run into issues!

  2. Can you proove that reversing again a reversed hlist yields back the same type as the original input? In pseudo-code,

let rev_twice : 'xs hlist -> 'xs hlist = fun xs -> rev (rev xs)

I’m being a little fuzzy on purpose, the solutions are easier if you allow some leaway in the spec: for example it’s already great if you can show that the rev permutation has an inverse! (without going through the trouble of prooving that it is an involution)


For context, this problem comes up when implementing a breadth-first map over a GADT:

Oleg Kiselyov has a really nice explanation of the algorithms in “Breadth-first labelling” (which is a really fun puzzle!) In a more general setting, this is asking to evaluate the monadic parts of this applicative in breadth-first order:

module Make (M : MONAD) : sig
  type 'a t =
    | Pure : 'a -> 'a t
    | Map2 : ('a -> 'b -> 'c) * 'a t M.t * 'b t M.t -> 'c t

  val breadth_first : 'a t M.t -> 'a M.t
end

The algorithm naturally asks for a queue, which can be simulated by two lists (but the extra-spicy polymorphism here turns them into hlists). The double-rev typing puzzle shows up in between two levels of the tree. Quoting Kiselyov’s code:

| ([], next) -> let (next', []) = bfa_forests f (List.rev next, []) in
                ([], List.rev next')

… Well okay, I’m not saying that you are going to run into this in real-life, but it’s not entirely gratuitous either :slight_smile:

2 Likes

Very nice, thanks for the puzzle!
I’m curious to hear if you had something in mind simpler (or more clever) than what I came up with:

type nil = NIL
type _ hlist =
  | Nil : nil hlist
  | Cons : 'x * 'xs hlist -> ('x * 'xs) hlist

(* The easiest way of defining [rev] is as a special case of
   [rev_append]. Let's define [rev_append] on hlists.

   For that, we need to define a version of [rev_append] at the type
   level, to be able to type [rev_append]. It is expressed as a
   predicate, where [(a, b, c) isrevappend] means that [c] corresponds
   to [rev_append a b] (at the type level). *)

type (_, _, _) isrevappend =
| RAnil : (nil, 'a, 'a) isrevappend
| RAcons : ('a, 'x * 'b, 'c) isrevappend -> ('x * 'a, 'b, 'c) isrevappend

let _ : (string * (int * (float * nil)),
         nil,
         float * (int * (string * nil)))
    isrevappend
  = RAcons (RAcons (RAcons RAnil))

(* The [rev_append] function returns an existential package of an
   hlist as well as the witness that its type corresponds to the
   rev_append of the input types. *)

type (_, _) erevappend =
  | Erevappend : 'c hlist * ('a, 'b, 'c) isrevappend -> ('a, 'b) erevappend

let rec revappend : type a b. a hlist -> b hlist -> (a, b) erevappend =
  fun l1 l2 ->
  match l1 with
  | Nil -> Erevappend (l2, RAnil)
  | Cons (x, xs) ->
    let Erevappend (l', pf) = revappend xs (Cons (x, l2)) in
    Erevappend (l', RAcons pf)

(* [isrev] corresponds to rev_appending to an empty list *)

type ('a, 'b) isrev = ('a, nil, 'b) isrevappend

(* we can thus easily write [rev]. *)
type _ erev =
  | Erev : 'b hlist * ('a, 'b) isrev -> 'a erev

let rev : type a. a hlist -> a erev =
  fun l ->
  let Erevappend (l', pf) = revappend l Nil in
  Erev (l', pf)


(* Let's now prove that [rev (rev l) = l].

   Since our base working definition is not [isrev] but [isrevappend],
   we need a version of this lemma for [isrevappend].

   Let's prove the following:

   rev_append (rev_append a b) c = rev_append b (append a c)

   i.e:

   rev (rev a ++ b) ++ c = rev b ++ (a ++ c).

   Then we will specialize this theorem by picking b and c to be empty
   lists, and obtain that [rev (rev a) = a] as a corrolary.


   For that we need to define [isappend] as an auxiliary definition.
*)

type (_, _, _) isappend =
  | Anil : (nil, 'a, 'a) isappend
  | Acons : ('a, 'b, 'c) isappend -> ('x * 'a, 'b, 'x * 'c) isappend

let _ : (string * (int * nil), float * (unit * nil),
         string * (int * (float * (unit * nil)))) isappend =
  Acons (Acons Anil)

(* a first lemma: appending a list to the empty list gives the same
   list *)

type (_, _) eq = Eq : ('a, 'a) eq

let rec append_nil : type a b. (a, nil, b) isappend -> (a, b) eq =
  fun a ->
  match a with
  | Anil -> Eq
  | Acons a' -> let Eq = append_nil a' in Eq

(* let's now prove the main lemma *)

type (_, _, _, _) erevappendtwice =
  Erevappendtwice :
    ('a, 'c, 'ac) isappend *
    ('b, 'ac, 'r) isrevappend ->
    ('a, 'b, 'c, 'r) erevappendtwice

(*
rev (rev a ++ b) ++ c
=
rev b ++ (a ++ c)
*)
let rec revappend_twice : type a b c r1 r2 r3 ac.
  (a, b, r1) isrevappend ->
  (r1, c, r2) isrevappend ->
  (a, b, c, r2) erevappendtwice
=
fun ra1 ra2 ->
match ra1 with
| RAnil ->
  (* a = nil, r1 = b *)
  Erevappendtwice (Anil, ra2)

| RAcons ra1' ->
  (* a = $0 * $1
     ra1' = ($1, $0 * b, r1) isrevappend
  *)
  let Erevappendtwice (app, RAcons r) = revappend_twice ra1' ra2 in
  Erevappendtwice (Acons app, r)

(* phew. *)

(* we can now specialize the lemma to prove that [isrev] is idempotent
*)

let rev_twice : type a b c.
  (a, b) isrev ->
  (b, c) isrev ->
  (a, c) eq
=
  fun r1 r2 ->
  let Erevappendtwice (app, RAnil) = revappend_twice r1 r2 in
  let Eq = append_nil app in
  Eq

(* and invoke this to implement [rev_twice] *)

let rev_twice : type a. a hlist -> a hlist =
  fun l ->
  let Erev (l', r) = rev l in
  let Erev (l'', r') = rev l' in
  let Eq = rev_twice r r' in
  l''

3 Likes

Wow that was fast, well done!

And no not really, my solution is very similar with a slightly different lemma:

type (_, _, _) revappend =
  | Rnil  : (nil, 'ys, 'ys) revappend
  | Rcons : ('xs, 'x * 'ys, 'zs) revappend -> ('x * 'xs, 'ys, 'zs) revappend

(* (xs, ys, zs) rev_append   means   rev xs ++ ys == zs *)

type ('xs, 'ys) isrev = ('xs, nil, 'ys) revappend   (* rev xs == ys *)

(* rev xs == ys  ==>  rev ys == xs *)
let rev_flip : type xs ys. (xs, ys) isrev -> (ys, xs) isrev
= fun r ->
  (*     rev a ++ b == ys
     /\  rev b ++ a == xs
     ==> rev ys == xs

     ie.  rev (rev a ++ b) == rev b ++ rev (rev a)
                           == rev b ++ a

     we can't actually use this proof since we don't
     have [rev (xs ++ ys) == rev ys ++ rev xs]
     or [rev (rev a) == a] ... but induction works!
  *)
  let rec go
  : type a b c. (a, b, ys) revappend -> (b, a, xs) revappend -> (ys, xs) isrev
  = fun left right ->
    match left with
    | Rnil -> right
    | Rcons left -> go left (Rcons right)
  in
  go r Rnil


(* the boring part: *)

type (_, _) eq = Refl : ('a, 'a) eq

let rec rev_eq
: type a b xs ys. (a, b, xs) revappend -> (a, b, ys) revappend -> (xs, ys) eq
= fun r1 r2 ->
  match r1, r2 with
  | Rnil, Rnil -> Refl
  | Rcons r1, Rcons r2 -> rev_eq r1 r2


(* and finally: *)

type _ rev_hlist = Rev : ('xs, 'ys) isrev * 'xs hlist -> 'ys rev_hlist

let rev : type xs. xs hlist -> xs rev_hlist
= fun xs ->
  let rec go : type a b. (a, b, xs) revappend -> a hlist -> b hlist -> xs rev_hlist
  = fun r acc -> function
    | Nil -> Rev (r, acc)
    | Cons (x, xs) -> go (Rcons r) (Cons (x, acc)) xs
  in
  go Rnil Nil xs

let rev_twice : type xs. xs hlist -> xs hlist
= fun xs ->
  let Rev (r1, ys) = rev xs in
  let Rev (r2, zs) = rev ys in
  let Refl = rev_eq r1 (rev_flip r2) in
  zs