Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Default implementations for instances

view this post on Zulip Email Gateway (Aug 19 2022 at 14:16):

From: Lars Hupel <hupel@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:16):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

  1. 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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:18):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The story is more complicated since a »definition« in general is not
necessarily equational. As example have a look at class
complete_lattice where Inf determines Sup and vice versa, but none is
characterized equationally in the class' assumes.

I hope someday that »permanent_interpretation« inside instantiation
targets yields a pattern for default instantiations, but this is music
of the future.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:18):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

  1. 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

signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:19):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

No, please do not triple the number of type classes. It is already now somewhat cumbersome
to instantiate the order type classes for some type 'a foo to get the right sort
constraints on the type parameter (things are already worse for the algebraic type classes).

instantiation foo :: (ord) ord ...
instance foo :: (preorder) preorder ...
instance foo :: (order) order ...
instance foo :: (linorder) linorder ...

If you split each of these type classes into three, one would have to write twelve
instance declarations and proofs.

My point was that such default implementations might be convenient for the order
hierarchy. By the way, another example of making constants to type class parameters for
the sake of code generation can be found in the card_UNIV hierarchy in
HOL/Library/Cardinality.

Andreas

Last updated: Nov 21 2024 at 12:39 UTC