Email Gateway (Aug 18 2022 at 12:53): Email Gateway (Aug 18 2022 at 12:53):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I have problems to instantiate the recpower class for parametric types.
E.g., I have defined substitutions as association lists from variables
to terms
types ('f,'v)sub = "('v * ('f,'v)term)list"
Now I want to instantiate `sub' for the recpower class where the unit
element is the empty substitution and multiplication is substitution
composition. But already for
instantiation sub :: recpower begin
I get Illegal type abbreviation: "Term.sub"'. What does that mean? Can
I only instantiate types defined by datatype'? How do I write the
instantiation for parametric types (if possible at all)?
cheers
christian sternagel
Email Gateway (Aug 18 2022 at 12:53):From: Alexander Krauss <krauss@in.tum.de>
Hi Chris,
Only real type constructors can be instances of classes. Sub is just a
type abbreviation. If you really need the instance, you must wrap up
your substitutions in a real datatype.
Alex
Email Gateway (Aug 18 2022 at 12:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian
"types" does only introduce a syntactic abbreviation, not a logical
type! If you want to use type classes, you have to provide a separate
logical type, in the extreme case as a mere copy, e.g.:
datatype ('f, 'v) sub = Sub "('v * ('f, 'v) term) list"
primrec dest_Sub where "dest_Sub (Sub xs) = xs"
instantiation sub :: recpower begin
...
Hope this helps
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC