Email Gateway (Aug 18 2022 at 12:26): Email Gateway (Aug 18 2022 at 12:26):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
Is there a way to partially define a datatype? Or, is there a way to
define it generally at one point, and then redefine/specialise it
later on?
I have some results which only require that I define my datatype as
datatype form = At "nat"
| Compound "string" "form list"
i.e. that I define formulae as atomic and compound, and can
distinguish between them. I would like to then specialise this
datatype somewhat, so for a particular application I may wish to have
Compound = Conj "form" "form"
| Disj "form" "form"
so then the datatype would be
At "nat"
Conj "form" "form"
Disj "form" "form"
and for another
Compound = neg "form"
| Impl "form" "form"
so the datatype would be
At "nat"
neg "form"
Impl "form" "form"
Obviously, I'd like the original results which I proved to hold for
the new datatype, which is a specialisation of the old one.
Essentially, I would like to plug in a more complete version of what
it means for a formula to be compound.
I've looked at the documentation about type classes and locales, but I
don't see how that would apply here: I'm not adding new operations to
a theory, just new constructors to a datatype.
Many thanks
Peter
Email Gateway (Aug 18 2022 at 12:26):From: Tobias Nipkow <nipkow@in.tum.de>
Peter, this sounds rather fanciful and I don't think there is an easy
solution. You cannot add constructors to a datatype (and you even want
to remove one). The best I can think of is to make the datatype more
generic:
datatype 'a form = At "nat" | Compound 'a "'a form list"
so you can instantiate it:
datatype condis = Con | Dis
types cd_form = "condis form"
However, this yields n-ary conjunctions and disjunctions; which becomes
awkward for negation ;-) So you would need an additional predicate for
wellformed formulae of certain kinds.
Tobias
Peter Chapman schrieb:
Email Gateway (Aug 18 2022 at 12:27):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
There is a simple, if clunky, alternative.
You could simply declare your new type (unfortunately, needing new names
for all the constructors), then declare an injection function that maps
from your new type to the subset of the old type that you are interested
in representing. You could then do all your logic on injections of values
in the new type.
It's the lowest-budget solution, and will probably allow you to get the
job done, but I suppose it isn't pretty. There may be a way to hide the
injection function and the renaming of the constructors using locales.
Yours,
Thomas.
Last updated: May 03 2024 at 12:27 UTC