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

*From*: "'Shon Feder' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Tue, 2 Aug 2022 10:37:15 -0700 (PDT)*References*: <c6213ec6-1261-4cc9-b646-9cda6c8d81d3n@googlegroups.com> <28caeb66-1ff0-4315-bd21-32d12040e08c@gmail.com> <f488aa2a-6ece-4e7a-b166-6daa396dd712n@googlegroups.com>

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

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

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`

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.

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/5ffd3692-f094-4c8b-8e70-30f290ac6c8fn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Modeling optional values - from a newbie***From:*Brandon Barker

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

**Re: [tlaplus] Modeling optional values - from a newbie***From:*Hillel Wayne

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

- Prev by Date:
**Re: [tlaplus] Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by Date:
**[tlaplus] Question about the value of action expressions** - Previous by thread:
**Re: [tlaplus] Modeling optional values - from a newbie** - Next by thread:
**Re: [tlaplus] Modeling optional values - from a newbie** - Index(es):