`var` type annotation: implicit sub‑tytping?

[Yannick Duchêne]

This:

        var a:int = 0

        var b:int = 1

        val () = ( a :=: b )

… does not type‑check. I get an error about an unsolved constraint [0 == 1].

However this:

        var a = 0:int

        var b = 1:int

        val () = ( a :=: b )

… type‑check with no error.

It’s like if the former was interpreted like this:

        var a:int(0) = 0

        var b:int(1) = 1

        val () = ( a :=: b )

Is this expected?

Here is what I got in my notes, not about `var` but about `val`, and I expected it to be the same with `var`.

> `val x = e:T`: typical of annotations, checks `e` is of type `T`.

> `val x:T = e`: checks type of `e` is of a subtype of `T`.

Instead of checking 0 or 1 is a subtype of int, it seems to assign `a` the `int(0)` subtype and `b`, the `int(1)` subtype.

Surprisingly, the JSON data says `a` and `b` are of type int, not `int(0)` and `int(1)`. This suggests the type annotation is modified at a later stage. Is this a bug or is this expected?

[Hongwei Xi]

This is a confusing part of ATS.

When (a :=: b) is performed, the values stored in a and b are

required to be of the same type.

Say you do

var a: int = 0

The type 'int' is referred to as the master type for 'a'; it is used

for allocating 'a'. The value in a is of the type int(0) as '0' without

annotation is given the type int(0).

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3104aa67-f91f-42f3-a396-f2565a0c684d%40googlegroups.com.

[Yannick Duchêne]

Le mardi 26 juin 2018 14:52:28 UTC+2, gmhwxi a écrit :

This is a confusing part of ATS.

When (a :=: b) is performed, the values stored in a and b are

required to be of the same type.

Say you do

var a: int = 0

The type 'int' is referred to as the master type for 'a'; it is used

for allocating 'a'. The value in a is of the type int(0) as '0' without

annotation is given the type int(0).

May be not that confusing. `a`  is container, what it holds has its own value. If the exchange operator was able to change this type, it could brake anything stated about something where `a` is involved, since it is allowed to assert something based on the exact sub‑type `a` holds. This is just sound.

What I forgot about, is that `0` is of type `int(0)` and so on (added in my notes, an old omission) …