Kenta Inoue (Oct 21 2021 at 01:32): Kenta Inoue (Oct 21 2021 at 01:32):Hi,
in the following code, Applicative.class_of can be compiled without Definition comp_pureMap_class_of ....
But, it is not compiled with the error The term "comp" has type "(?B2 -> ?A4) -> (?C -> ?B2) -> ?C -> ?A4" while it is expected to have type "?A3".
Why the type-check do not work well by adding comp_pureMap_class_of.
Module Pure.
Definition Eta (m:Type -> Type) := forall A, A -> m A.
Record class_of (m:Type -> Type) :=
Class {
eta : Eta m;
}.
Section Packing.
Structure map := Pack {apply; _: class_of apply}.
Variable (cF : map).
Definition class :=
let: Pack _ c := cF return class_of (apply cF) in c.
End Packing.
Module Exports.
Notation pureMap := map.
Notation Eta := Eta.
Coercion apply : map >-> Funclass.
Definition eta T := (eta (class T)).
End Exports.
End Pure.
Import Pure.Exports.
(* 1 *)
Definition comp_pureMap_class_of (m n:pureMap) : Pure.class_of (m \o n)
:= (Pure.Class (fun A => (@eta m _ \o @eta n A))).
(* 2 *)
Module Applicative.
Definition Applicative (m:Type -> Type)
:= forall A B, m (A -> B) -> m A -> m B.
Record class_of (m:Type -> Type) :=
Class {
base : Pure.class_of m;
applicative : Applicative m;
_: forall A B (f g:A -> B),
f =1 g ->
applicative (eta (Pure.Pack base) f)
=1 applicative (eta (Pure.Pack base) g);
_: forall A (x:m A),
applicative (eta (Pure.Pack base) id) x = x;
_: forall A B C (f:m (B -> C)) (g:m (A -> B)) x,
applicative (applicative
(applicative
(eta (Pure.Pack base) comp) f)
(* (@eta (Pure.Pack base)
((_ -> _) -> (_ -> _) -> _) comp) f)*)
g) x =
applicative f (applicative g x);
_: forall A B (f:A -> B) x,
applicative (eta (Pure.Pack base) f) (eta (Pure.Pack base) x) =
eta (Pure.Pack base) (f x);
_: forall A B (f:m (A -> B)) x,
applicative f (eta (Pure.Pack base) x) =
applicative (eta (Pure.Pack base) (@^~ x)) f
}.
End Applicative.
It’s not possible to step through your code as is, I think it lacks notations (\o and @^~) and something for implicit arguments at least? Could you provide those or an import so that we can try and debug it?
Ana de Almeida Borges (Oct 22 2021 at 10:39):Meven, it works with
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
This is a universe issue: defining comp_pureMap_class_of forces some constraints between the universe levels of comp and those of the other definitions you have around. There are at least two solutions: the easy one is to replace m \o n by fun x => m (n x) in the definition of comp_pureMap_class_of. A better solution to keep using comp would be to declare it universe polymorphic, which is not done in ssreflect for various technical reasons, but you could try and redefine your own.
Meven Lennon-Bertrand (Oct 22 2021 at 12:27):Using this should do the trick:
Polymorphic Definition comp {A B C} (f : B -> A) (g : C -> B) : C -> A :=
fun x => f (g x).
Notation "f1 \o f2" := (comp f1 f2) : fun_scope.
Last updated: Apr 19 2024 at 15:02 UTC