Sum types are subtly different from union types. To represent union types in TLC, I usually do something like this:
CONSTANT NotAnInt
ASSUME NotAnInt \notin Int
TypeInv ==
OptionalVal \in Int \union {NotAnInt}
To represent optionals as a sum type, I'd instead used a tagged
struct:
TypeInv ==
OptionVal \in [type: {"some"}, val: Nat] \union [type:
{"none"}]
H
--Some languages have optional data types (Scala's Option, Java's Optional, Haskell's Maybe, etc), the purpose of which is to obviate the need for null values. As a union type, it can be expressed like:
Option a = Some a | None
(so an Option of a type a is either a Some of a or it is None.
I was trying to think of a good way to do this in an untyped, set-theoretic setting, while trying to avoid accidental equivalence with other values, and came up with something a bit convoluted and arbitrary:
None == {{"a", {"fairly unique", {"id:", {"69a86178-6aba-445b-a74b-6769ff09cc29"}}}}}
some(x) == [some: x]
NatOption[x \in Nat] == [some: x] \union {None}
This seemed to cause errors in my relatively small, nascent spec once I ran TLC. Unfortunately, I didn't seem to get a line # for the error:
The exception was a java.lang.RuntimeException
: Attempted to compare the set {"69a86178-6aba-445b-a74b-6769ff09cc29"} with the value:
"id:"
I can try to come up with a a minimal example to reproduce, but maybe it is better to ask how others would model optional values (and types)?--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6213ec6-1261-4cc9-b646-9cda6c8d81d3n%40googlegroups.com.