# 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 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
``````