Re: [tlaplus] Re: Checking data type Pluscal

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

https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1997-006A.pdf

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.