Modeling optional values - from a newbie

[Brandon Barker]

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)?

[Felipe Oliveira Carvalho]

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.

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6213ec6-1261-4cc9-b646-9cda6c8d81d3n%40googlegroups.com.

[Leslie Lamport]

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.

Leslie

[Leslie Lamport]

Correction: that should have been "a TLC model" rather than "a TLA model".

L.

[Hillel Wayne]

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

[Brandon Barker]

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

[Shon Feder]

Sorry for the late addition here.

Apalache has recently added a Variants extension which provides syntactic support for sum types. This extension enables static analysis by Apalache's type checker, which can help catch erroneous use of sum types during specification. Under the hood, our encoding desugars down to something very similar to what Hillel has given.

You can use the extension to give a workable representation of a polymorphic option type, useful for representing partial computations.  While we haven't developed any battle tested libraries with convenience operators around this extension yet, the following example gives an indication of how those might look:

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

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

You can typecheck this spec in Apalache via `apalache-mc typecheck OptionExample.tla` and confirm that the values computed in the invariant hold with `apalache-mc check --inv=Inv OptionExample.tla`

[Brandon Barker]

Oh, thank you, I'm definitely looking forwad to trying Apalache. (As a personal bonus, I currently develop Scala code, which it is written in).

[Debersaques Laurent]

I've been trying to use Leslie's definition for  None:

   None == CHOOSE n : n \notin Nat

However, TLC emits an error when I add this definition to my spec. The error is:

   TLC attempted to evaluate an unbounded CHOOSE.
   Make sure that the expression is of form CHOOSE x \in S: P(x).

It seems TLC is unable to pick an arbitrary value if no bound is provided for n. It makes sense, but then I guess one might as well write

  CONSTANT None
  ASSUME None \notin Nat

and assign  None to an arbitrary string value when checking the model with TLC.

[Stephan Merz]

If you launch TLC from the Toolbox, it will automagically include a suitable replacement for None in the configuration file that it generates.

If you launch TLC from the command line or from the VS Code Extension, you'll have to do it yourself by including something like

None = None

in the CONSTANTS section of the configuration file. This mysteriously looking equation instructs TLC to substitute the model value [1] None for the operator None defined in the TLA+ module.

The alternative that you indicate of declaring a constant parameter and assumption is also idiomatic. It still makes sense to instantiate that constant by a model value when you run TLC.

Stephan

[1] See Specifying Systems, section 14.2.1, for more explanations.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57aff553-fb2d-486f-8dc6-54524be0c034n%40googlegroups.com.

[Laurent Debersaques]

Thank you for the thorough explanation. 

Section 14.2.1 of the book does clear things up.