The Coq mailing list

[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