(In)Equality and conjunction and type mismatch

Google Group
1

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.

2

‘==’ 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.

3

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.

4

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.

5

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

I agree.

6

This one?

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/fixity.ats

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

7

This one?

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> 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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at 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?utm_medium=email&utm_source=footer
.

8

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

9

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.

10

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