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

Google Group
1

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?

2

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.On Tuesday, May 19, 2015 at 7:49:13 PM UTC-4, Yannick Duchêne wrote:

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?

3

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).

4

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.On Tuesday, May 19, 2015 at 2:57:12 PM UTC-4, Yannick Duchêne wrote:

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?

5

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?