[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Modeling optional values - from a newbie

The mathematical way to define None to be a value that is not a natural number is:

   None == CHOOSE n : n \notin Nat

I believe that if you then create a TLA model for the spec, that model will substitute for None what is called a model value that TLC considers to be unequal to any value other than None.


On Friday, July 29, 2022 at 5:37:19 PM UTC-7 brandon...@xxxxxxxxx wrote:
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:

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/c123ba98-0951-4486-a9c0-23056acada61n%40googlegroups.com.