Checking data type Pluscal

[christin...@gmail.com]

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!

[Andrew Helwer]

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

[Hillel Wayne]

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

--
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/9fd4aa9c-e599-4ca1-ac9d-868e41235518n%40googlegroups.com.

[Andrew Helwer]

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

[Calvin Loncaric]

> 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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4224ab06-be44-4eb3-b925-49dd294c1d26n%40googlegroups.com.