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

*From*: Felipe Oliveira Carvalho <felipekde@xxxxxxxxx>*Date*: Fri, 29 Jul 2022 21:49:38 -0300*References*: <c6213ec6-1261-4cc9-b646-9cda6c8d81d3n@googlegroups.com>

Whenever I needed to model optionals I tried to find a sentinel value that could represent None: 0, -1, empty string.

When that's not possible I would use a unitary set containing the value and the empty set to represent None. This actually leads to quite nice spec code. For instance: no need to unpack an optional when "adding" it to a set with many values — it's just union.

On Fri, 29 Jul 2022 at 21:37 Brandon Barker <brandon.barker@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:

"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.

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/CAOC8YXb5L9Nn3GsqmWA0yD%2B31GJ%3DsuX4yDobgtFPk9jEWvm_-A%40mail.gmail.com.

**References**:**[tlaplus] Modeling optional values - from a newbie***From:*Brandon Barker

- Prev by Date:
**[tlaplus] Modeling optional values - from a newbie** - Next by Date:
**[tlaplus] Re: Modeling optional values - from a newbie** - Previous by thread:
**[tlaplus] Modeling optional values - from a newbie** - Next by thread:
**[tlaplus] Re: Modeling optional values - from a newbie** - Index(es):