Re: [isabelle] Default implementations for instances



> The most prominent example of this probably is "op <" in the preorder
> type class, which is completely determined by the assumption
> strict_iff_order. All instantiations have to specify both "op <=" and
> "op <" and prove that they are compatible. The theory Partial_Function
> even defines a general mk_less operator to that end.

This strict coupling of Orderings.less_eq and Orderings.less is mainly
historic and could be split into two class hierarchies (e.g. strict_*
and reflexive_*, where the existing class »foo« joins the classes
strict_foo and reflexive_foo).

If the situation is pressing enough, this should be seriously considered.

Cheers,
	Florian

> 
> 2. In my AFP entry Containers, I introduce a new typeclass clinorder
> which has a default implementation if the type is in linorder, and the
> same for ceq and HOL.equal. René Thiemann extended his
> Datatype_Order_Generator such that it can automatically produce these
> instantiations and discharge the proof obligations.
> 
> However, in this setting, I would not want to the instance to be
> automatic. Rather do I want to decide when I pick the default
> implementation and when I choose some other implementation. This would
> mean that I still issue a command that triggers the default
> implementation, but I no longer have to specify the instantiation nor
> prove the assumptions.
> 
> Note that in this case, the assumptions are not of the form "f = foo g".
> 
> Andreas
> 
> On 10/04/14 16:16, Lars Hupel wrote:
>> Assume the following classes:
>>
>> class a =
>>    fixes f :: "'a => nat"
>>    assumes ...
>>
>> class b =
>>    fixes g :: "'a => 'a => nat"
>>    assumes ...
>>
>> (the precise types of the class parameters don't matter)
>>
>> Furthermore assume that 'f' can be implemented in terms of 'g', but
>> not all types can be
>> made instances of class 'b'. In such a case, I would like to define a
>> subclass
>> relationship between 'b' and 'a', but this doesn't work (because 'f'
>> is not a class
>> parameter of 'g').
>>
>> Johannes showed me the following "pattern" which is used e.g. in
>> Real_Vector_Space:
>>
>> class a0 =
>>    fixes f :: "'a => nat"
>>
>> class a =
>>    assumes ...
>>
>> class b = a0 +
>>    assumes "f = foo g" (* the implementation of 'f' in terms of 'g' *)
>>    and ...
>> begin
>>
>>    subclass a
>>    proof ...
>>
>> end
>>
>> This works well, but comes at the cost of having to duplicate the 'f =
>> foo g' line in
>> every instantiation of some type for 'b'. Additionally, when using
>> 'f', type inference
>> will give me a class constraint 'a0' which does not carry the
>> necessary assumptions.
>>
>> My question now is whether this is common enough that it warrants a
>> "default
>> implementation" mechanism, in the sense that one could specify the
>> implementation of 'f'
>> in terms of 'g' "once and for all", and not having to define and prove
>> it everywhere. This
>> could potentially also make sense if just one class is involved:
>>
>> class eq =
>>    fixes eq  :: "'a => 'a => bool"
>>      and neq :: "'a => 'a => bool"
>>    assumes "neq x y <--> ~(eq x y)"
>>
>>
>> Lars
>>

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.