The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi Victor,
The more I read your questions the more I think you don't understand
Coq Type Classes.
Coq Classes/Structure is not C++ Classes.
The labels in a class are projector functions not fields: for example
with your Base Class, set is
a function which takes a Base and extracts its first component. It is
not a field of a C++ class,
so it really doesn't need this / self or whatever.

This line makes no sense to me: mygraph: set->set->Prop.
set is a function, not a type. Maybe you intended to write
Definition mygraph (b: Base) := set b -> set b -> Prop  ?

Please try to read an introduction book to type classes (or ask more question
on your thread about what is a type classes).

Best,
Vincent

2011/11/6 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
>