# (In)Equality and conjunction and type mismatch

**URL:** <https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538>\
**Category:** Google Group\
**Created:** [February 5, 2015, 1:14pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538 "2015-02-05T13:14:06Z")\
**Posts on this page:** 10\
**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:** [February 5, 2015, 1:14pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/1 "2015-02-05T13:14:06Z")

</div>

Hello,

I must be clumsy in some way, but I have questions about the cases below.

Both type‑checks:

```
 fn test {x:int} (x:int(x)): bool(x <= 0) = (x <= 0) /* Case 1.a */
 fn test {x:int} (x:int(x)): bool(0 <= x) = (0 <= x) /* Case 1.b */

```

This one don’t for a reason which is mysterious to me, unless it’s related  
to the case after:

```
 fn test {x:int} (x:int(x)): bool(x <= 0 && 0 <= x) = (x <= 0 && 0 <= 

```

x) /\* Case 2 \*/

This is in fact equivalent to this, which fails too, for a reason looking  
more obvious to me:

```
 fn test {x:int} (x:int(x)): bool(x == 0) = (x == 0) /* Case 3 */

```

In case #3, `0` is not of the type `int(x)`, unless `x` is zero, which is  
not always the case. However, if I do the following, I still get an error:

```
 fn test {x:int|x==0} (x:int(x)): bool(x == 0) = (x == 0) /* Case 4 */

```

I feel to understand why case #3 fails (while not sure I really understand  
the reason), but not why case #4 fails too.

I also wonder if ATS is turning case #2 into case #3.

---

<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:** [February 5, 2015, 5:52pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/2 "2015-02-05T17:52:44Z")

</div>

> ‘==’ is not used in the dynamics. Please use ‘=’ instead. For Case 4, you  
> can actually have:

And I’m learning this so late (red face). And the same for `&&` ?

So I should update my colorizer about `=` which is handled as a keyword, as  
I though it was used for assignment only. But I’m afraid it must be hard to  
properly makes a distinction between `=` for assignment and `=` as an  
operator.

Anyway, I will have a closer look at operators restricted to static and  
dynamic, I’m not enough aware of it.

---

<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:** [February 5, 2015, 6:35pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/3 "2015-02-05T18:35:57Z")

</div>

Yes, = is both a keyword and a special operator.

Right now, ‘==’ is idle. If you like, you can add the following macro:

macdef ==(x, y) = (,(x) = ,(y))

ATS largely follows the ML tradition:

= for equality  
:= for assignment

In ML, == is often used for reference equality.On Thursday, February 5, 2015 at 12:52:46 PM UTC-5, Yannick Duchêne wrote:

> Le jeudi 5 février 2015 17:28:08 UTC+1, gmhwxi a écrit :
> 
> > ‘==’ is not used in the dynamics. Please use ‘=’ instead. For Case 4, you  
> > can actually have:
> 
> And I’m learning this so late (red face). And the same for `&&` ?
> 
> So I should update my colorizer about `=` which is handled as a keyword,  
> as I though it was used for assignment only. But I’m afraid it must be hard  
> to properly makes a distinction between `=` for assignment and `=` as an  
> operator.
> 
> Anyway, I will have a closer look at operators restricted to static and  
> dynamic, I’m not enough aware of it.

---

<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:** [February 5, 2015, 7:47pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/4 "2015-02-05T19:47:58Z")

</div>

> 

> > Yes, = is both a keyword and a special operator.
> > 
> > Right now, ‘==’ is idle. If you like, you can add the following macro:
> > 
> > macdef ==(x, y) = (,(x) = ,(y))
> 
> It works, that’s nice. What about adding this in the default environment  
> which ATS automatically loads? Or would this break something?

I did use == for reference quality somewhere in my code. Personally, I  
prefer = over == as it is the symbol used in mathematics.

> ATS largely follows the ML tradition:
> 
> > = for equality  
> > := for assignment
> 
> For assignment as side effect, only. I don’t know if “val x = y” can  
> properly be called an assignment or if there is a better word (formally,  
> that’s a declaration).

This is usually referred to as name binding (or simply binding) in  
functional programming: Think of x as a name for the value of y.

---

<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:** [February 5, 2015, 8:11pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/5 "2015-02-05T20:11:47Z")

</div>

> I did use == for reference quality somewhere in my code. Personally, I  
> prefer = over == as it is the symbol used in mathematics.

I agree.

---

<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:** [February 7, 2015, 12:24am UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/6 "2015-02-07T00:24:31Z")

</div>

> This one?
> 
> [https://github.com/githwxi/ATS-Postiats/blob/master/prelude/fixity.ats](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/fixity.ats)

This one 😛  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2221.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2221.html) (I  
just retrieved it)

---

<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:** [February 6, 2015, 1:27am UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/7 "2015-02-06T01:27:26Z")

</div>

This one?

[https://github.com/githwxi/ATS-Postiats/blob/master/prelude/fixity.atsOn](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/fixity.atsOn) Thu, Feb 5, 2015 at 7:45 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Talking about operators, I remember I’ve seen a page in ATS docs, listing  
> predefined operators. I’m not able to retrieve it. It was on the ATS site,  
> not on the wiki. Do you or someone else, see what page it is and can post  
> its URL?
> 
> Le jeudi 5 février 2015 19:35:57 UTC+1, gmhwxi a écrit :
> 
> > Yes, = is both a keyword and a special operator.
> > 
> > Right now, ‘==’ is idle. If you like, you can add the following macro:
> > 
> > macdef ==(x, y) = (,(x) = ,(y))
> > 
> > ATS largely follows the ML tradition:
> > 
> > = for equality  
> > := for assignment
> > 
> > In ML, == is often used for reference equality.
> > 
> > On Thursday, February 5, 2015 at 12:52:46 PM UTC-5, Yannick Duchêne wrote:
> > 
> > > Le jeudi 5 février 2015 17:28:08 UTC+1, gmhwxi a écrit :
> > > 
> > > > ‘==’ is not used in the dynamics. Please use ‘=’ instead. For Case 4,  
> > > > you can actually have:
> > > 
> > > And I’m learning this so late (red face). And the same for `&&` ?
> > > 
> > > So I should update my colorizer about `=` which is handled as a keyword,  
> > > as I though it was used for assignment only. But I’m afraid it must be hard  
> > > to properly makes a distinction between `=` for assignment and `=` as an  
> > > operator.
> > > 
> > > Anyway, I will have a closer look at operators restricted to static and  
> > > dynamic, I’m not enough aware of it.
> > > 
> > > –  
> > > 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-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/c233f355-aba7-4e20-8418-397c5b392b87%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/c233f355-aba7-4e20-8418-397c5b392b87%40googlegroups.com)  
> > > [https://groups.google.com/d/msgid/ats-lang-users/c233f355-aba7-4e20-8418-397c5b392b87%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/c233f355-aba7-4e20-8418-397c5b392b87%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > .

---

<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:** [February 5, 2015, 4:28pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/8 "2015-02-05T16:28:08Z")

</div>

&& is a macro:

macdef &&(x, y) = (if x then y else false): bool

To get what you want, please replace && with \*.

The following code typechecks:

fn test {x:int} (x:int(x)): bool(x \<= 0) = (x \<= 0) /\* Case 1.a _/  
fn test {x:int} (x:int(x)): bool(0 \<= x) = (0 \<= x) /_ Case 1.b \*/

fn test {x:int} (x:int(x)): bool(x \<= 0 && 0 \<= x) = (x \<= 0) \* (0 \<= x) /\*  
Case 2 \*/

fn test {x:int} (x:int(x)): bool(x == 0) = (x = 0) /\* Case 3 \*/

fn test {x:int|x==0} (x:int(x)): bool(x == 0) = (x = 0) /\* Case 4 \*/

‘==’ is not used in the dynamics. Please use ‘=’ instead. For Case 4, you  
can actually have:

fn test {x:int|x==0} (x:int(x)): bool(true) = (x = 0) /\* Case 4 \*/On Thursday, February 5, 2015 at 8:14:06 AM UTC-5, Yannick Duchêne wrote:

> Hello,
> 
> I must be clumsy in some way, but I have questions about the cases below.
> 
> Both type‑checks:
> 
> ```
> fn test {x:int} (x:int(x)): bool(x <= 0) = (x <= 0) /* Case 1.a */
> fn test {x:int} (x:int(x)): bool(0 <= x) = (0 <= x) /* Case 1.b */
> 
> ```
> 
> This one don’t for a reason which is mysterious to me, unless it’s related  
> to the case after:
> 
> ```
> fn test {x:int} (x:int(x)): bool(x <= 0 && 0 <= x) = (x <= 0 && 0 <= 
> 
> ```
> 
> x) /\* Case 2 \*/
> 
> This is in fact equivalent to this, which fails too, for a reason looking  
> more obvious to me:
> 
> ```
> fn test {x:int} (x:int(x)): bool(x == 0) = (x == 0) /* Case 3 */
> 
> ```
> 
> In case #3, `0` is not of the type `int(x)`, unless `x` is zero, which is  
> not always the case. However, if I do the following, I still get an error:
> 
> ```
> fn test {x:int|x==0} (x:int(x)): bool(x == 0) = (x == 0) /* Case 4 */
> 
> ```
> 
> I feel to understand why case #3 fails (while not sure I really understand  
> the reason), but not why case #4 fails too.
> 
> I also wonder if ATS is turning case #2 into case #3.

---

<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:** [February 6, 2015, 12:45am UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/9 "2015-02-06T00:45:57Z")

</div>

Talking about operators, I remember I’ve seen a page in ATS docs, listing  
predefined operators. I’m not able to retrieve it. It was on the ATS site,  
not on the wiki. Do you or someone else, see what page it is and can post  
its URL?Le jeudi 5 février 2015 19:35:57 UTC+1, gmhwxi a écrit :

> Yes, = is both a keyword and a special operator.
> 
> Right now, ‘==’ is idle. If you like, you can add the following macro:
> 
> macdef ==(x, y) = (,(x) = ,(y))
> 
> ATS largely follows the ML tradition:
> 
> = for equality  
> := for assignment
> 
> In ML, == is often used for reference equality.
> 
> On Thursday, February 5, 2015 at 12:52:46 PM UTC-5, Yannick Duchêne wrote:
> 
> > Le jeudi 5 février 2015 17:28:08 UTC+1, gmhwxi a écrit :
> > 
> > > ‘==’ is not used in the dynamics. Please use ‘=’ instead. For Case 4,  
> > > you can actually have:
> > 
> > And I’m learning this so late (red face). And the same for `&&` ?
> > 
> > So I should update my colorizer about `=` which is handled as a keyword,  
> > as I though it was used for assignment only. But I’m afraid it must be hard  
> > to properly makes a distinction between `=` for assignment and `=` as an  
> > operator.
> > 
> > Anyway, I will have a closer look at operators restricted to static and  
> > dynamic, I’m not enough aware of 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:** [February 5, 2015, 7:18pm UTC](https://discourse.ats-lang.org/t/in-equality-and-conjunction-and-type-mismatch/538/10 "2015-02-05T19:18:03Z")

</div>

> Yes, = is both a keyword and a special operator.
> 
> Right now, ‘==’ is idle. If you like, you can add the following macro:
> 
> macdef ==(x, y) = (,(x) = ,(y))

It works, that’s nice. What about adding this in the default environment  
which ATS automatically loads? Or would this break something?

> ATS largely follows the ML tradition:
> 
> = for equality  
> := for assignment

For assignment as side effect, only. I don’t know if “val x = y” can  
properly be called an assignment or if there is a better word (formally,  
that’s a declaration).