(In)Equality and conjunction and type mismatch

[Yannick Duchêne]

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.

[gmhwxi]

&& 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 */


[Yannick Duchêne]

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.

[gmhwxi]

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.

[Yannick Duchêne]

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

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

[gmhwxi]

On Thursday, February 5, 2015 at 2:18:03 PM UTC-5, Yannick Duchêne wrote:

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

 

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.
 

[Yannick Duchêne]

Le jeudi 5 février 2015 20:47:58 UTC+1, gmhwxi a écrit :

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

I agree. 

[Yannick Duchêne]

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 :

[Hongwei Xi]

This one?

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

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

[Yannick Duchêne]

Le vendredi 6 février 2015 02:27:27 UTC+1, gmhwxi a écrit :

This one?

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

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