Re: [isabelle] Making records instances of classes

Hello Peter,

> Is it possible to make a record type an instance of a type class?
yes, it is, but you must have a look behind the scenes. The Isabelle record package provides extensible records. You could define a subrecord of Tuple with additional fields and the record package ensures subtyping, i.e. every element of the subrecord type works almost like an ordinary Tuple record, in particular, cast operations work as expected.

Behind the scenes, the package achieves this by defining a more general type for Tuple called Tuple_ext_type, which takes another type variable. Then, the type ('a, 'b) Tuple is just a type abbreviation for ('a, 'b, unit) Tuple_ext_type. For subrecord types, this additional type variable is instantiated to some other type which stores the additional information.

Type classes can only be instantiated for "logical" type constructors, not for abbreviations like Tuple. In your example, you would have to instantiate Tuple_ext_type itself. Note that this instantiation then also applies to all subrecords you might ever define.

record ('a, 'b) Tuple = first :: "'a" second :: "'b"

instance Tuple_type_ext :: (finite, finite, finite) finite


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

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