The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Oh, I found a working solution, using @. But to find it was not trivial. We 
need to update Coq code or at least to describe this trick in Coq 
documentation:

Classes.v:
[[[
Class Base := {
  set: Set
}.
]]]

RelTypes.v"
[[[
Require Import Classes.
Require Import sset2.

Class Relation := {
  relation_is_base :> Base;
  (*mygraph: set->set->Prop*)
  mygraph: Set;
  is_rel: is_graph mygraph
}.

Definition compose_relation_classes (f g: Relation) := (compose_graph 
(@mygraph f) (@mygraph g)).

Class Reflexive := {
  reflexive_is_relation :> Relation;
  is_reflexive: forall x:Set, ((inc x set)->(related mygraph x x))
}.

Class Symmetric := {
  symmetric_is_relation :> Relation;
  is_symmetric: forall x y:Set, ((related mygraph x y)<->(related mygraph y 
x))
}.
]]]

06.11.2011, 04:52, "Victor Porton" 
<porton AT narod.ru>:
> My proposal:
>
> If a definition receives more than one argument of a class, the class 
> should behave as if it would be a structure.
>
> This would make this code working:
>
> Definition compose_relation_classes (f g: Relation) := (compose_graph 
> (mygraph f) (mygraph g)).
>
> Experts, does my proposal sound good? Any alternative solutions?
>
> 06.11.2011, 04:48, "Victor Porton" 
>Â <porton AT narod.ru>:
>
>> šOops, I noticed that the below works if I replace Structure -> Class.
>>
>> šBut if I replace structures with classes, then the commented definition 
>> below stops working:
>>
>> šDefinition compose_relation_classes (f g: Relation) := (compose_graph 
>> (mygraph f) (mygraph g)).
>>
>> šSo either one or the other does not work. Coq type classes need a 
>> redesign!
>>
>> š06.11.2011, 04:24, "Victor Porton" 
>>Â <porton AT narod.ru>:
>>> ššClasses.v:
>>> šš[[[
>>> ššStructure Base := {
>>> ššššset: Set
>>> šš}.
>>> šš]]]
>>>
>>> ššRelTypes.v:
>>> šš[[[
>>> ššRequire Import Classes.
>>> ššRequire Import sset2.
>>>
>>> ššStructure Relation := {
>>> ššššrelation_is_base :> Base;
>>> šššš(*mygraph: set->set->Prop*)
>>> ššššmygraph: Set;
>>> ššššis_rel: is_graph mygraph
>>> šš}.
>>>
>>> šš(*Definition compose_relation_classes (f g: Relation) := (compose_graph 
>>> (mygraph f) (mygraph g)).*)
>>>
>>> ššClass Reflexive := {
>>> ššššreflexive_is_relation :> Relation;
>>> ššššis_reflexive: forall x:Set, ((inc x set)->(related mygraph x x))
>>> šš}.
>>> šš]]]
>>>
>>> ššThis produces the error:
>>>
>>> ššThe term "set" has type "Base -> Set" while it is expected to have type 
>>> "Set".
>>>
>>> ššThus I see no way to specify that in the definition of the class 
>>> Reflexive "set" should refer to the current instance of the class rather 
>>> than to be considered as an un-applied function of type "Base -> Set".
>>>
>>> ššWe need some good way to deal with this trouble. For instance, we may 
>>> introduce a new keyword (self, this, our, etc.) which will denote the 
>>> current class instance.
>>>
>>> ššIn Reference Manual type classes are marked as an experimental feature. 
>>> It is really so. Type classes do not work as expected in Coq 8.3pl2.
>>>
>>> ššI want to wait for the next version. Meanwhile I do not like to use Coq 
>>> because its classes are broken.
>>>
>>> šš--
>>> ššVictor Porton - http://portonvictor.org
>> š--
>> šVictor Porton - http://portonvictor.org
> --
> Victor Porton - http://portonvictor.org

-- 
Victor Porton - http://portonvictor.org