The Coq mailing list

[Max Schaefer <xiemaisi AT yahoo.de>]

(* 
Hi all,

here's a cute little trick for using the type class mechanism to implement
annotation-free typesafe casts that I'd like to share with you.

This post is a Coq (8.2) script, so let's set up some things first.
*)
Set Implicit Arguments.
Require Import Program.Tactics.
Require Import Omega.

(*
Let's look at everybody's favourite example of a dependent data structure:
length indexed vectors.
*)
Inductive vec A : nat -> Type :=
  | vnil : vec A 0
  | vcons : forall n, A -> vec A n -> vec A (S n).

(*
We all know that the append function for such vectors practically writes 
itself:
*)
Fixpoint app A m n (v:vec A m) (w:vec A n) :=
  match v in vec _ m return vec A (m+n) with
    | vnil => w
    | vcons _ x xs => vcons x (app xs w)
  end.

(*
Unfortunately, this is less true of other functions. For example, we might 
want to implement reverse as follows:

  Fixpoint rev A n (v:vec A n) :=
    match v in vec _ n return vec A n with
      | vnil => vnil A
      | vcons _ x xs => app (rev xs) (vcons x (vnil A))
    end.

but Coq will complain that the term in the second branch of match has type
vec A (n+1), whereas it's supposed to be vec A (S n).

One way to solve this is to note that Coq already provides a very powerful
cast operator.
*)
Check eq_rect : forall (A:Type) (x:A) (P:A->Type), P x -> forall (y:A), x=y 
-> P y.

(*
We can certainly prove that n+1 = S n, so if we take P := fun n => vec A n 
then eq_rect will behave like a cast from vec A (n+1) to vec A n.

Unfortunately, using eq_rect directly is a bit clumsy, since one needs to at 
least supply P and a proof of x=y, which leads to noisy code. Instead, we'll 
define a cast operator that uses maximally inserted arguments and type 
classes to automatically infer these two arguments whenever possible.
*)

(*
We need to reflect equalities into the world of type classes to make them 
available for type class instance proof search.
*)
Class Equal (A:Type) (x y:A) := {
  equal : x = y
}.

(*
Here is a simple instance of this class.
*)
Instance Refl A (x:A) : Equal x x := {
  equal := refl_equal _
}.

(*
The following two will come in handy for dependent types. They prove 
substitutivity in operand and operator position, respectively.
*)
Instance Leibniz A B (x y:A) (H:Equal x y) (f:A->B) : Equal (f x) (f y) := {
  equal := eq_rect x (fun y => f x = f y) (refl_equal _) y equal
}.

Instance FunSubst A B (f f':A->B) (H:Equal f f') (a:A) : Equal (f a) (f' a) 
:= {
  equal := eq_rect f (fun f' => f a = f' a) (refl_equal _) f' equal
}.

(*
Our implementation of cast is very simple: To safely cast an element x from 
type A to type B, we require an instance of Equal A B, which contains a proof 
of A=B. This proof gets plugged into eq_rect.
*)
Definition cast A {B} {H:Equal A B} (x:A) : B :=
  eq_rect A (fun t=>t) x B equal.
(*
We certainly want the type class proof search to find the equality proof for 
us, hence H is maximally inserted, but it will also be convenient to have B 
be maximally inserted, since it can usually be deduced from the context.
*)

(*
Remember that in the case of rev above, we wanted to cast from Vec A (n+1) to 
Vec A (S n). So we first prove that their indices are equal.
*)
Program Instance PlusOneEqS : forall n, Equal (n+1) (S n).
Next Obligation. omega. Defined.

(*
And now we can write rev almost like we wanted to, just inserting a cast 
(without any annotations!) around the second branch of the match.
*)
Fixpoint rev A n (v:vec A n) :=
  match v in vec _ n return vec A n with
    | vnil => vnil A
    | vcons _ x xs => cast (app (rev xs) (vcons x (vnil A)))
  end.
(*
Coq can infer from the context that the cast must be of type vec A (S n), and 
it uses the instance declarations PlusOneEqS and Leibniz to construct an 
instance of Equal (vec A (n+1)) (vec A (S n)), which is supplied as argument 
H to the cast function.
*)

(*
Of course this also works with more complex types...
*)
Require Import List.
Parameter T1 : list nat -> Type.
Parameter T2 : list nat -> nat -> Type.

(*
...and more complex equalities.
*)
Program Instance PushLastRight : forall A (l:list A) x r, Equal 
((l++x::nil)++r) (l++x::r).
Next Obligation. induction l; simpl; f_equal; auto. Defined.

(*
Assuming the following...
*)
Variables l r : list nat.
Variable n : nat.
Variable x : T1 ((l++n::nil)++r).
Variable y : T2 ((l++n::nil)++r) 23.

(*
...we get:
*)
Check (cast x : T1 (l++n::r)).
Check (cast y : T2 (l++n::r) 23).

(*
Note that we can use Coq's _:_ notation to conveniently provide an 
instantiation for B if we need to.
*)

(*
So what we get is a completely annotation-free type cast; we only need to 
declare an instance of class Equal for every equality that we'd like the cast 
to be able to use.

Two caveats apply:

- Under the hood, your terms will still be littered with eq_rects that may 
block reduction and can generally get quite obnoxious. This is not the 
problem we're trying to solve here.

- There are certain instance declarations that will make proof search very 
slow. For instance, declaring an instance for Symmetry will lead to much 
larger proof terms, and declaring an instance for commutativity of addition 
seemed to lead to an infinite loop on my machine. It's probably possible to 
tweak the proof search algorithm to handle this more gracefully (Matthieu?).

That's it for now, hope you enjoyed it.

All the best,
-- Max
*)