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

If you are not too familiar with GADTs, then the first puzzle is to type the
rev
function, sinceval rev : 'xs hlist > ??? hlist
is going to run into issues! 
Can you proove that reversing again a reversed hlist yields back the same type as the original input? In pseudocode,
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 breadthfirst map over a GADT:
Oleg Kiselyov has a really nice explanation of the algorithms in “Breadthfirst labelling” (which is a really fun puzzle!) In a more general setting, this is asking to evaluate the monadic parts of this applicative in breadthfirst 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 extraspicy polymorphism here turns them into hlists). The doublerev 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 reallife, but it’s not entirely gratuitous either