INV in ATS2

Google Group
1

Just curious what INV means.

Thanks,
Brandon

2

A type.On Thu, Jun 18, 2015 at 11:37 PM, Kiwamu Okabe kiw...@gmail.com wrote:

On Wednesday, July 10, 2013 at 2:35:33 AM UTC+9, gmhwxi wrote:

fun{a:t@ype} foo (xs: list0 (INV(a))): void

Assume that mylst is of the type list0 (T) for some T.
When typechecking foo(mylst), the typechecker will expand
the expression as follows by picking a placeholder T1:

foo(mylst)

where T <= T1 is assumed.

What is “T1”?

–
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/2acc15f3-ffba-40fd-b5c2-e99db819e94e%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/2acc15f3-ffba-40fd-b5c2-e99db819e94e%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

Right. It is typo as you pointed out.

4

The reason is that there are many possibilities, all of which can be
“correct”.

For instance, cons(10, nil) can have infinitely many types:

list(int, 1)
list(int(10), 1)
list(intGte(10), 1)

Without INV, the programmer has to pass types explicitly.

Is it correct to understand it as a bit similar to the “like” clause in
Eiffel?

5

fun{a:t@ype} foo (xs: list0 (INV(a))): void

Assume that mylst is of the type list0 (T) for some T.
When typechecking foo(mylst), the typechecker will expand
the expression as follows by picking a placeholder T1:

foo(mylst)

where T <= T1 is assumed.

What is “T1”?

6

You can but it does not work here.
The above example should be written as follows:

fun{} pal_empty{a:t@ype} …On Thu, Jun 18, 2015 at 11:52 PM, Kiwamu Okabe kiw...@gmail.com wrote:

On Friday, June 19, 2015 at 12:44:45 PM UTC+9, Kiwamu Okabe wrote:

In conclusion, ATS’s template engine can’t guess correct type variable
without INV?

May I set INV into return value of function such like following?

fun{a:t@ype} pal_empty
(): (PAL (ilist_nil) | gflist (INV(a), ilist_nil ()))

–
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/2972bcb5-80df-475f-ab7d-736ba4a66376%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/2972bcb5-80df-475f-ab7d-736ba4a66376%40googlegroups.com?utm_medium=email&utm_source=footer
.

7

So I think this comes full circle to my very first question about ATS:
http://sourceforge.net/mailarchive/forum.php?thread_name=alpine.LRH.2.02.1302120729160.29395%40csa2.bu.edu&forum_name=ats-lang-users

If this is the case, I believe there is just a minor typo in your example
above, where foo should not use INV:

fun{a:t@ype} foo (xs: list0 (a)): void

This seems like a good feature to know about! Perhaps even more interesting
is thinking of ways to use the absence of INV, by learning uses of
covariant types.

8

The reason is that there are many possibilities, all of which can be
“correct”.

For instance, cons(10, nil) can have infinitely many types:

list(int, 1)
list(int(10), 1)
list(intGte(10), 1)

Without INV, the programmer has to pass types explicitly.
…On Thu, Jun 18, 2015 at 11:44 PM, Kiwamu Okabe kiw...@debian.or.jp wrote:

On Fri, Jun 19, 2015 at 12:40 PM, Hongwei Xi gmh...@gmail.com wrote:

A type.

Umm…
In conclusion, ATS’s template engine can’t guess correct type variable
without INV?

Kiwamu Okabe at METASEPI DESIGN

–
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/CAEvX6dk7yM9sdi31VXoRZooiHxY1aAibkjtnGSn__-4XD7cjAw%40mail.gmail.com
.

9

INV is for invariant.

It is essentially marker for typechecking.

For instance, say you have a funtion foo
declared as follows:

fun{a:t@ype} foo (xs: list0 (INV(a))): void

Assume that mylst is of the type list0 (T) for some T.
When typechecking foo(mylst), the typechecker will expand
the expression as follows by picking a placeholder T1:

foo(mylst)

where T <= T1 is assumed.

Say that foo2 is declared as follows:

fun{a:t@ype} foo2 (xs: list0 (INV(a))): void

When foo2(mylst) is typechecked, the typechecker simply
expands the expression to foo2(mylst).

10

In conclusion, ATS’s template engine can’t guess correct type variable
without INV?

May I set INV into return value of function such like following?

fun{a:t@ype} pal_empty
(): (PAL (ilist_nil) | gflist (INV(a), ilist_nil ()))

11

I just see it as some sort of syntactic annotation
for the purpose of simplifying contraint-solving:

If the following constraint is encountered:

INV(X) <= T (where X is a unification variable),

then it is automatically turned into (X = T).On Sunday, August 23, 2015 at 5:41:40 PM UTC-4, Yannick Duchêne wrote:

Le vendredi 19 juin 2015 05:51:08 UTC+2, gmhwxi a écrit :

The reason is that there are many possibilities, all of which can be
“correct”.

For instance, cons(10, nil) can have infinitely many types:

list(int, 1)
list(int(10), 1)
list(intGte(10), 1)

Without INV, the programmer has to pass types explicitly.

Is it correct to understand it as a bit similar to the “like” clause in
Eiffel?