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

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

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

  ASSUME None \notin Nat

and assign  None to an arbitrary string value when checking the model with TLC.
On Friday, 5 August 2022 at 16:08:11 UTC+2 Brandon Barker wrote:

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).
On Tuesday, August 2, 2022 at 1:37:15 PM UTC-4 sh...@informal.systems wrote:
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;

\* @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)
  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`
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:

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"}]


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:

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.

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/57aff553-fb2d-486f-8dc6-54524be0c034n%40googlegroups.com.