# Is \`a: some\_type\` a boolean expression? (or of sort boolean)

**URL:** <https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682>\
**Category:** Google Group\
**Created:** [May 19, 2015, 6:57pm UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682 "2015-05-19T18:57:11Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 19, 2015, 6:57pm UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682/1 "2015-05-19T18:57:11Z")

</div>

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](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?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 20, 2015, 12:52am UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682/2 "2015-05-20T00:52:19Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 19, 2015, 11:36pm UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682/3 "2015-05-19T23:36:20Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 19, 2015, 11:13pm UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682/4 "2015-05-19T23:13:04Z")

</div>

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](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?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 19, 2015, 11:49pm UTC](https://discourse.ats-lang.org/t/is-a-some-type-a-boolean-expression-or-of-sort-boolean/682/5 "2015-05-19T23:49:13Z")

</div>

> 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?