Email Gateway (Aug 18 2022 at 15:37): Email Gateway (Aug 18 2022 at 15:37):From: Peter Gammie <peteg42@gmail.com>
Hello,
Is it possible to make a record type an instance of a type class?
Here's a simple example of what doesn't work:
record ('a, 'b) Tuple = first :: "'a" second :: "'b"
instance Tuple :: (finite, finite) finite
*** Logical type constructor expected: "t.Tuple"
*** At command "instance" (line 7 of "/tmp/t.thy").
cheers
peter
Email Gateway (Aug 18 2022 at 15:38):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Cheers,
Andreas
Email Gateway (Aug 18 2022 at 15:38):From: Peter Gammie <peteg42@gmail.com>
Thanks Andreas!
Perhaps this could make its way into the distributed Isabelle documentation and/or examples?
Also Florian Haftmann sent me this complete chunk of proof text off-list, for which I am grateful:
record ('a, 'b) Tuple = first :: "'a" second :: "'b"
instance Tuple_ext_type :: (finite, finite, finite) finite
proof
let ?U = "UNIV :: ('a, 'b, 'c) Tuple_ext_type set"
{ fix x :: "('a, 'b, 'c) Tuple_scheme"
have "∃a b c. x = Tuple_ext a b c"
by (cases x) simp
} then have U:
"?U = (\<lambda>((a, b), c). Tuple_ext a b c) ` ((UNIV × UNIV) × UNIV)"
by (auto simp add: image_def)
show "finite ?U" by (simp add: U)
qed
cheers
peter
Email Gateway (Aug 18 2022 at 17:26):From: Philipp Küfner <philipp.kuefner@tu-berlin.de>
Dear all,
In July 2010 there was a discussion on Making records instances of
classes. As far as I can see the presented solution (see below) does not
work with the current version of Isabelle (2011) anymore (due to the new
implementation of records). So does anyone know how to handle this
problem now?
Thanks a lot,
Philipp
Thanks Andreas!
Perhaps this could make its way into the distributed Isabelle documentation and/or examples?
Also Florian Haftmann sent me this complete chunk of proof text off-list, for which I am grateful:
record ('a, 'b) Tuple = first :: "'a" second :: "'b"
instance Tuple_ext_type :: (finite, finite, finite) finite
proof
let ?U = "UNIV :: ('a, 'b, 'c) Tuple_ext_type set"
{ fix x :: "('a, 'b, 'c) Tuple_scheme"
have "∃a b c. x = Tuple_ext a b c"
by (cases x) simp
} then have U:
"?U = (\<lambda>((a, b), c). Tuple_ext a b c) ` ((UNIV × UNIV) × UNIV)"
by (auto simp add: image_def)
show "finite ?U" by (simp add: U)
qed
cheers
peter
Email Gateway (Aug 18 2022 at 17:26):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Philipp,
in Isabelle 2011, the type for extensible records is no longer called
<record name>_type_ext, but <record name>_ext. The NEWS file mentions this as
follows:
- Records: logical foundation type for records does not carry a
'_type' suffix any longer (obsolete due to authentic syntax).
INCOMPATIBILITY.
Hence, the following should work now:
record ('a, 'b) Tuple = first :: "'a" second :: "'b"
instance Tuple_ext :: (finite, finite, finite) finite
Hope this helps,
Andreas
Philipp Küfner schrieb:
Email Gateway (Aug 18 2022 at 17:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Philipp,
the solution to your problem is to drop the _type suffix on the record
type name.
This is what the (for end-users rather cryptic, I confess) entry in the
NEWS file:
hints at.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC