Email Gateway (Aug 19 2022 at 11:35): Email Gateway (Aug 19 2022 at 11:35):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
this is analogous to the approach taken in functional languages such as
Haskell: you can define a type class (e.g. "getval") that defines a
getval function of the appropriate type and then declare type class
instances for your two datatypes. This way, you get something akin to
overloading in Java. But let us not talk about the Java type system.
If you don't know how to do use type classes in Isabelle, you can find
lots of examples in the Isabelle theory library; off the top of my head,
I vaguely remember something like this being done for a function
extracting variables from boolean and arithmetic expressions in IMP,
that could serve as an example.
Of course, there is also the type class tutorial by Florian Haftmann:
http://isabelle.in.tum.de/dist/Isabelle2013/doc/classes.pdf
Regarding the second question, I'm not entirely sure if I understood
that correctly, but if I have, the only way to do this that I can think
of is also by incorporating a function that does this into the type
class and then writing appropriate instances for your datatypes.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:44):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi all,
Let's say I have two datatypes:
datatype 't t1 = C1a 't | C1b 't option
datatype 't t2 = C2a 't | C2b 't option
Then let's say that for a common 'y type, I have two elements e1 of type 'y t1 and e2 of type 'y t2.
let us finally say there is a value v such that e1 = C1a v and e2 = C2a v.
How could I define a "getval" function such that getval e1 = getval e2 is a admissible expression ? What type would it have ? It sounds like Java overloading, but I do not reckon there is such a thing in Isabelle, am I wrong ?
Secondly, is there any way I could say that some element e, which type could be either t1 or t2, is such that getval e = Some v, without having to say wether C1b or C2b was used to define it ?
Thanks in advance !
H.
Last updated: Apr 16 2024 at 12:28 UTC