Re: [tlaplus] Modeling optional values

------------------- MODULE OptionExample -----------------------
EXTENDS Naturals, Apalache, Variants

\* @type: UNIT;
UNIT == "U_OF_UNIT"

\* @typeAlias: option = Some(a) | None(UNIT);

\* @type: a => $option;
Some(x) == Variant("Some", x)
\* @type: () => $option;
None == Variant("None", UNIT)

\* @type: $option => Bool;
IsSome(o) == VariantTag(o) = "Some"
\* @type: $option => Bool;
IsNone(o) == VariantTag(o) = "None"

\* @type: $option => a;
GetUnsafe(o) == VariantGetUnsafe("Some", o)

\* @type: (a => b, $option) => $option;
OptionMap(f(_), o) ==
IF IsSome(o)
THEN Some(f(GetUnsafe(o)))
ELSE None

\* @type: Set(a) => $option;
MaxSet(s) ==
LET max(oa, b) ==
IF IsNone(oa)
THEN Some(b)
ELSE IF GetUnsafe(oa) > b THEN oa ELSE Some(b)
IN
ApaFoldSet(max, None, s)

Init == TRUE
Next == TRUE
Inv ==
/\ OptionMap(LAMBDA x: x + 1, Some(2)) = Some(3)
/\ OptionMap(LAMBDA x: x + 1, None) = None
/\ OptionMap(LAMBDA s: s \union {"B"}, Some({"A"})) = Some({"A", "B"})
/\ MaxSet({1,3,4,2}) = Some(4)
/\ MaxSet({}) = None

============================================================

On Monday, August 1, 2022 at 2:45:06 PM UTC-4 brandon...@xxxxxxxxx wrote:

Thanks all, for the replies, they were all helpful in my understanding.

On Saturday, July 30, 2022 at 3:19:54 AM UTC-4 hwa...@xxxxxxxxx wrote:

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

On 7/29/2022 7:37 PM, Brandon Barker 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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6213ec6-1261-4cc9-b646-9cda6c8d81d3n%40googlegroups.com.

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