How do I refer to type-polymorphic type variables in the type theorem?
I wrote a Functor
Haskell type class :
Class Functor (f: Type -> Type) := { map {a b: Type}: (a -> b) -> (f a -> f b); map_id: forall (a: Type) (x: f a), map id x = x }
Where id
has an obvious definition.
Now I have discovered the instances Functor
for list
and the type of the function. But I want to prove the statements about any functor. First, I want to prove that there is essentially a tautology: repetition map_id
for any functor.
Theorem map_id_restatement: forall (F: Type -> Type), Functor F -> forall T (x: F T), map id x = x.
The idea was to prove this theorem, I would just apply map_id
. But I get an error when I try to prove it:
Toplevel input, characters 88-91: Error: Could not find an instance for "Functor F" in environment: F : Type -> Type T : Type x : F T
But the instance Functor F
must already be in scope because of the type assumption. Why isn't it recognized?
Edit:
OK, I figured out I can get it to work, quantitatively Functor F
:
Theorem map_id_restatement: forall (F: Type -> Type) (finst: Functor F), forall T (x: F T), map id x = x. Proof. apply @map_id. Qed.
Why is this necessary? Interestingly, it doesn't work unless I explicitly provide the name of the functor instance (i.e. if I just write (_: Functor F)
).
source to share
I don't know if this is a bug or not, but note that when you write something like Functor F -> SomeType
you are implicitly stating that it is SomeType
not instance dependent Functor
, which is not true in your case: the complete type of your theorem, printing all implicit arguments, would be something like this:
Theorem map_id_restatement: forall (F: Type -> Type) (finst: Functor F), forall T (x: F T), @map F fints T T (@id T) x = x.
If you replace finst
with _
, you get
Theorem map_id_restatement: forall (F: Type -> Type) (_: Functor F), forall T (x: F T), @map F _ T T (@id T) x = x.
which cannot be type checked because _
it is not a variable name.
Note that if you bind Functor F
anonymously before the colon, Coq accepts it:
Theorem map_id_restatement (F: Type -> Type) (_ : Functor F) : forall T (x: F T), map (@id T) x = x. Proof. apply @map_id. Qed.
Presumably, here Coq handles it _
differently and replaces it with an auto-generated name instead of actually leaving it unnamed. You can also use the following form, which works both under forall
and before the colon:
Theorem map_id_restatement (F: Type -> Type) : forall `(Functor F), forall T (x: F T), map (@id T) x = x. Proof. apply @map_id. Qed.
source to share