Jun Xu (Apr 25 2026 at 04:58): Jun Xu (Apr 25 2026 at 04:58):Hi all,
I have a small programming language with a type system. The types are encoded as a datatype Typ := TNum | TBool | TFn Typ Typ. I wish to assign denotational semantic domains to each (recursive) type.
I have a data structure "'a lattice" where the underlying set has elements of type 'a. Hence, the assignment of semantic domains would be "nat lattice" for TNum, or "bool lattice" for TBool. Now a problem arises: I cannot define an Isabelle function "semantic_domain:: Typ -> _" that does this, because "nat lattice" and "bool lattice" are different types and are rejected by Isabelle.
There is a workaround for this, which is creating a corresponding value datatype Val := VNum nat | VBool bool | VFn Val => Val, then make "semantic_domain:: Typ -> Val lattice". Then I will have to distinguish different kinds of Val lattice.
My question is: is there an alternative way that does not involve creating a Val datatype?
Alex Mobius (Apr 25 2026 at 09:34):Ran into the same issue! No, Isabelle doesn't have that. You can either define an Any type like you said here, and/or have projection functions to different concrete types which are only going to be defined for specific Typ. (You could also have a polymorphic constant Typ => 'a lattice with each overload only defined for one Typ)
Last updated: May 01 2026 at 16:59 UTC