Is `a: some_type` a boolean expression? (or of sort boolean)

[Yannick Duchêne]

Hi there,

I was at studying possible variations of a proposal from Artyom Shalkhakov, in https://groups.google.com/d/msg/ats-lang-users/_7E45-45sXA/4Jf-HiFXu44J , when I faced a unexpected assertion from ATS (I don't want to say ATS is wrong, just that it's me who was surprised).

In short, I wanted to attach a proposition to a type instead of returning a proposition along with a value of this type (for convenience only, I will finally try to achieve this convience another way, but this is a another question).

Schematically, I had these steps (the conclusion and the related question comes later):

First, I declared an abstract proposition:

absprop PROP(int)

I wanted to have something different than

typedef special_int = [i: int] (PROP(i) | int i)

I had a naive attempt to attach it to a `typedef`, this alternative wrong way:

typedef special_int = [i: int | PROP(i)] int i

ATS complained `PROP(i)` is of sort `prop`, while it is expected to be of sort `bool`.

So I naively attempted to workaround it, this as much bad way:

typedef special_int = [i: int] [PROP(i) | true] int i

ATS complained the same… looks like it tells me at that place too, a boolean expression is expected, to my surprise.

I wanted to check if it indeed was, thinking: if it expects a boolean expression at the place `PROP(i)` was in the second attempt, this means the `a: some_type` are boolean expressions too, as this is what normally appears on the left side of `|` in quantifiers, and so this could as much appears on the right side, where ATS expects a boolean expression too (less surprisingly).

So I tried this:

typedef special_int = [i: int] [j: int | k: int] int i

ATS does not complains, and type‑check it…

Does it really means `i: int` and the likes are expressions of sort boolean?

If yes, what means the `k: int` above, as a predicate?

[gmhwxi]

Note that [i:int | k:int] is the same as [i:int;k:int].
In particular, '|' is really the same as ';'.

Inside [...] (and {...}), two kinds of items are allowed:
a quantified variable (e.g., i:int) or a boolean expression (e.g., i > j).
These items need to be separated either by ';' or '|'; there is no difference
as to whether '|' or ';' is used.

[Yannick Duchêne]

Le mercredi 20 mai 2015 01:13:04 UTC+2, gmhwxi a écrit :

Note that [i:int | k:int] is the same as [i:int;k:int].
In particular, '|' is really the same as ';'.

Was worth asked… now I have a regret for not giving this thread a more significant title (but I could not guess).

 

So starting from now, when I will use `;` to make a distinction with the `|` used to separate proof/prop values and regular value. It happens I was wondering why the same symbol was used, now I know there are unrelated in these two distinct uses.

Inside [...] (and {...}), two kinds of items are allowed:
a quantified variable (e.g., i:int) or a boolean expression (e.g., i > j).
These items need to be separated either by ';' or '|'; there is no difference
as to whether '|' or ';' is used.

So that was just the checker which made a not best guess about the error :-p (it choose one among two, and it was not the best one).

[Yannick Duchêne]

Le mercredi 20 mai 2015 01:13:04 UTC+2, gmhwxi a écrit :

Note that [i:int | k:int] is the same as [i:int;k:int].
In particular, '|' is really the same as ';'.

Inside [...] (and {...}), two kinds of items are allowed:
a quantified variable (e.g., i:int) or a boolean expression (e.g., i > j).
These items need to be separated either by ';' or '|'; there is no difference
as to whether '|' or ';' is used.

And when it contains only boolean expression(s), (i.e. no static variable declarations, which may be declared elsewhere), I suppose it makes no difference weither it is inside `[]` or inside `{}`? Isn't it?

[gmhwxi]

There is a HUGE difference.

{i > 0} (...) means that (i > 0) must be true in order for (...) to be used.
So it is like  (i > 0) => (...); this form of type is called guarded type.

[i > 0] (...) is like (i > 0) /\ (...); this form of type is called asserting type.

[Yannick Duchêne]

Le mercredi 20 mai 2015 02:52:19 UTC+2, gmhwxi a écrit :

There is a HUGE difference.

{i > 0} (...) means that (i > 0) must be true in order for (...) to be used.
So it is like  (i > 0) => (...); this form of type is called guarded type.

[i > 0] (...) is like (i > 0) /\ (...); this form of type is called asserting type.

It’s more tricky than it looks when it is overlooked.

Given this type definition:

        typedef t(i:int) = {i == 0} int(i)

Then given these instantiations:

        val a: t(2) = 1

        val b: t(1) = 1

        val c: t(0) = 1

… only the last one does not type‑check.

It seems it reads like this: “if i is 0, then int(i) else int”.

Wondering, for a check I tested this:

        val d: t(1) = 'A'

… which (luckily or not) does not type‑check, meaning it does not exactly reads as a material implication, since if it did, then when `i == 0` is false, what follows `=>` could be anything and this test shows it can’t. Or else, “anything” is to be read as `int` instead of `int(i)`, that is, any int.

 

[Yannick Duchêne]

Although `{e} t(i)` makes sense, `[e] t(i)` is probably what one wants most of time. The former should be looked at carefully.

[Hongwei Xi]

Absolutely.

When using {e} t(i), you can think of it as a function: {e} () -> t(i).

On Thu, Jun 21, 2018 at 6:28 AM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:

Although `{e} t(i)` makes sense, `[e] t(i)` is probably what one wants most of time. The former should be looked at carefully.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5f898ea3-8539-4162-ba5b-aed6938660d6%40googlegroups.com.