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

*From*: Calvin Loncaric <c.a.loncaric@xxxxxxxxx>*Date*: Sun, 30 Jul 2023 13:58:13 -0700*References*: <697b7d3e-8321-4919-b257-8eb8df1959b7n@googlegroups.com> <9fd4aa9c-e599-4ca1-ac9d-868e41235518n@googlegroups.com> <05b51ed4-95f2-9cad-e672-4b5e503aa8cb@gmail.com> <4224ab06-be44-4eb3-b925-49dd294c1d26n@googlegroups.com>

> Is there a built in function to check the type of a variable in Pluscal?

As Andrew and Hillel noted, it does not.

More surprisingly, you cannot implement such a function, since different types like Int and STRING might not be disjoint.

For example, in TLA+ and PlusCal, the _expression_

1 = "one"

is not necessarily FALSE. It could be TRUE! It is definitely either TRUE or FALSE, but we can't know which one. Lamport calls these "silly" expressions, because the properties we care about should not depend on whether 1 = "one".

For expressions like 1 = "one", TLC does throw an error. This is the most sensible choice, since it would be wrong to return TRUE and it would be wrong to return FALSE---but in some sense, an error is also wrong, since that _expression_ has some definite---but unknowable---boolean value. Notably, there is no TLA+ or PlusCal construct for catching and handling that error. TLC is telling you "I don't know the answer", not "the answer is error", which is a subtle but important distinction.

This was initially very confusing for me, since I come from a programming background. How could 1 = "one" be TRUE? For more info, I highly recommend section 1.1 ("Untypes") of this tech report on The Operators of TLA+:

--

Calvin

On Sun, Jul 30, 2023 at 11:08 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

Interesting, I would say that seems like a bug but there is probably some performance-related reason why it doesn't work that way.Andrew--On Saturday, July 29, 2023 at 10:50:51 AM UTC-4 Hillel Wayne wrote:

TLC, though, effectively has types. If you check x \in Nat and x is a string, then TLC won't return FALSE, it will raise an error.H

On 7/29/2023 8:57 AM, Andrew Helwer wrote:

TLA+ and PlusCal don’t really have types. You can check for things like x \in Nat or x \in BOOLEAN to see whether it is in a given set of values.

Andrew

On Tuesday, July 25, 2023 at 9:41:50 PM UTC-4 christin...@xxxxxxxxx wrote:

Is there a built in function to check the type of a variable in Pluscal? Something similar to typeid in c++? I've tried searching but I can't find anything.

Thanks in advance!--

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/9fd4aa9c-e599-4ca1-ac9d-868e41235518n%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/4224ab06-be44-4eb3-b925-49dd294c1d26n%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/CABf5HMi2ufg3T4dL-bB7hrW4a8DvuGc4Au0rYEpt1NGmod9GUA%40mail.gmail.com.

**References**:**[tlaplus] Checking data type Pluscal***From:*christin...@xxxxxxxxx

**[tlaplus] Re: Checking data type Pluscal***From:*Andrew Helwer

**Re: [tlaplus] Re: Checking data type Pluscal***From:*Hillel Wayne

**Re: [tlaplus] Re: Checking data type Pluscal***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Re: Checking data type Pluscal** - Next by Date:
**Re: [tlaplus] Verifying c++ templates** - Previous by thread:
**Re: [tlaplus] Re: Checking data type Pluscal** - Next by thread:
**[tlaplus] A recreative spec, as a learn-by-doing thing.** - Index(es):