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