3 small clarification of the inductive definition of phantom.

Georges Gonthier and François Garillot are doing interesting things with phantom types and unification in Coq to allow one to write, for example, directv (V + W) to mean the proposition that $V \oplus W$ is a direct sum.

I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on. What is happening is that directv X is really notation for directv_def _ (Phantom _ X).

Phantom is a constructor of a very trivial inductive type

Inductive phantom (A:Type) (a:A) : Type := Phantom : phantom A a


The function Phantom is a polymorphic constructor of type forall (A:Type)(a:A), phantom A a. The purpose of Phantom is to lift values to the type level so that type inference can operate on these values.

directv_def doesn't even use the (Phantom _ X) argument (because it contains no data). The only purpose of this argument is to drive the type inference engine to fill in the first argument. directv_def has type forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop. addv_expr is a record type.

Record addv_expr := build_addv_expr {
V1 : VectorSpace;
V2 : VectorSpace;


The definition of directv_def is

directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)


The final ingredient is that fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2)) is declared as a Canoncial Structure.

So what does Coq read when you write directv (V + W)? Well it parses this as notation for

directv_def _ (Phantom _ (V + W))


The first parameter to Phantom is the type of (V + W) so we can quickly fill that in to get

directv_def _ (Phantom VectorSpace (V + W))


Phantom VectorSpace (V + W) has type phantom VectorSpace (V + W), but directv_def is expecting something of type phantom _ (Vadd _) so it tries to unify (V + W) with (Vadd _). Because Vadd is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose Vadd field is of the form (V + W). It says, "ahha! there is! I can use build_addv_expr V W (V + W)" (notice the intensional behaviour of canonical inference here). So Coq successfully unifies (V + W) with (Vadd (build_addv_expr V W (V + W)), and this forces the first parameter of directv_def:

directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))


And that is it for type inference. Later on this expression might be used, so it will start normalizing:

dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W)))


and then to

dim V + dim W = dim (V + W)


If you try to write something else like directv 0 then the canonical structure inference will fail and you will get a (probably obtuse) type error.

This has been as simplified example. In reality, directv is much more complicated and allows one to write directv (\sum_(0 <= i < n) V i) to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like directv 0 to mean a trivial direct sum.

Matita allows you to write unification hints directly without the necessarily building canonical structures. I suspect doing this sort of intentional inference would be easier in such a system.

2 fixing unmatched braces

Georges Gonthier and François Garillot are doing interesting things with phantom types and unification to allow one to write, for example, directv (V + W) to mean the proposition that $V \oplus W$ is a direct sum.

I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on. What is happening is that directv X is really notation for directv_def _ (Phantom _ X).

Phantom is a constructor of a very trivial inductive type

Inductive phantom (A:Type) (a:A) := Phantom : phantom A a


The function Phantom is a polymorphic constructor of type forall (A:Type)(a:A), phantom A a. The purpose of Phantom is to lift values to the type level so that type inference can operate on these values.

directv_def doesn't even use the (Phantom _ X) argument (because it contains no data). The only purpose of this argument is to drive the type inference engine to fill in the first argument. directv_def has type forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop. addv_expr is a record type.

Record addv_expr := build_addv_expr {
V1 : VectorSpace;
V2 : VectorSpace;


The definition of directv_def is

directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)


The final ingredient is that fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2)) is declared as a Canoncial Structure.

So what does Coq read when you write directv (V + W)? Well it parses this as notation for

directv_def _ (Phantom _ (V + W))


The first parameter to Phantom is the type of (V + W) so we can quickly fill that in to get

directv_def _ (Phantom VectorSpace (V + W))


Phantom VectorSpace (V + W) has type phantom VectorSpace (V + W)W), but directv_def is expecting something of type phantom _ (Vadd _))) so it tries to unify (V + W) with (Vadd _). Because Vadd is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose Vadd field is of the form (V + W). It says, "ahha! there is! I can use build_addv_expr V W (V + W)" (notice the intensional behaviour of canonical inference here). So Coq successfully unifies (V + W) with (Vadd (build_addv_expr V W (V + W)), and this forces the first parameter of directv_def:

directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))


And that is it for type inference. Later on this expression might be used, so it will start normalizing:

dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W)))


and then to

dim V + dim W = dim (V + W)


If you try to write something else like directv 0 then the canonical structure inference will fail and you will get a (probably obtuse) type error.

This has been as simplified example. In reality, directv is much more complicated and allows one to write directv (\sum_(0 <= i < n) V i) to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like directv 0 to mean a trivial direct sum.

Matita allows you to write unification hints directly without the necessarily building canonical structures. I suspect doing this sort of intentional inference would be easier in such a system.

1

Georges Gonthier and François Garillot are doing interesting things with phantom types and unification to allow one to write, for example, directv (V + W) to mean the proposition that $V \oplus W$ is a direct sum.

I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on. What is happening is that directv X is really notation for directv_def _ (Phantom _ X).

Phantom is a constructor of a very trivial inductive type

Inductive phantom (A:Type) (a:A) := Phantom : phantom A a


The function Phantom is a polymorphic constructor of type forall (A:Type)(a:A), phantom A a. The purpose of Phantom is to lift values to the type level so that type inference can operate on these values.

directv_def doesn't even use the (Phantom _ X) argument (because it contains no data). The only purpose of this argument is to drive the type inference engine to fill in the first argument. directv_def has type forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop. addv_expr is a record type.

Record addv_expr := build_addv_expr {
V1 : VectorSpace;
V2 : VectorSpace;


The definition of directv_def is

directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)


The final ingredient is that fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2)) is declared as a Canoncial Structure.

So what does Coq read when you write directv (V + W)? Well it parses this as notation for

directv_def _ (Phantom _ (V + W))


The first parameter to Phantom is the type of (V + W) so we can quickly fill that in to get

directv_def _ (Phantom VectorSpace (V + W))


Phantom VectorSpace (V + W) has type phantom VectorSpace (V + W)), but directv_def is expecting something of type phantom _ (Vadd _)) so it tries to unify (V + W) with (Vadd _). Because Vadd is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose Vadd field is of the form (V + W). It says, "ahha! there is! I can use build_addv_expr V W (V + W)" (notice the intensional behaviour of canonical inference here). So Coq successfully unifies (V + W) with (Vadd (build_addv_expr V W (V + W)), and this forces the first parameter of directv_def:

directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))


And that is it for type inference. Later on this expression might be used, so it will start normalizing:

dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W)))


and then to

dim V + dim W = dim (V + W)


If you try to write something else like directv 0 then the canonical structure inference will fail and you will get a (probably obtuse) type error.

This has been as simplified example. In reality, directv is much more complicated and allows one to write directv (\sum_(0 <= i < n) V i) to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like directv 0 to mean a trivial direct sum.

Matita allows you to write unification hints directly without the necessarily building canonical structures. I suspect doing this sort of intentional inference would be easier in such a system.