Re: [isabelle] Default implementations for instances



Hi Florian,

On 11/04/14 15:46, Florian Haftmann wrote:
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.
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




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