INV in ATS2

[Brandon Barker]

Just curious what INV means.

Thanks,

Brandon

[gmhwxi]

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<T1>(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<T>(mylst).

[Brandon Barker]

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.

[gmhwxi]

Right. It is typo as you pointed out.

[Kiwamu Okabe]

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<T1>(mylst)

where T <= T1 is assumed.

What is "T1"?
 

[Hongwei Xi]

A type.

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

[Kiwamu Okabe]

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

[Hongwei Xi]

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.

....

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

[Kiwamu Okabe]

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

[Hongwei Xi]

You can but it does not work here.

The above example should be written as follows:

fun{} pal_empty{a:t@ype} ...

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

[Yannick Duchêne]

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?

[gmhwxi]

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