Re: [isabelle] Default implementations for instances



Hi Lars,

I have longed for a similar mechanism for default implementations in two situations:

1. In the context of code generation, one often introduces a type class with a parameter whose assumptions completely determine the parameter. As parameters of type classes may have type-specific code equations, this is the only way to implement a polymorphic constant for each individual type.

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.

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





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