Subtyping?

Google Group
1

Hi all,

There are several mentions of covariance/contravariance in the
Introduction to Programming in ATS, but I don’t recall anything else
about what makes one type a subtype of another. Is it just a matter of
predicates on sorts, so nat n is a subtype of int n? Or is it something
more complicated?

Thanks,
Shea

P.S. I am not sure which group is appropriate to post to.

2

It is just a matter of predicates on type indices.

Assume:

typedef Pos = [a:int | a > 0] int(a)
typedef Nat = [a:int | a >= 0] int(a)

Pos is a subtype of Nat since (a > 0) implies (a >= 0)

Also, there are some built-in subtyping relations. For instance,

int(n) is a subtype of int (un-indexed); bool(b) is a subtype of
bool (un-indexed); etc.On Friday, August 29, 2014 5:25:23 PM UTC-4, Shea Levy wrote:

Hi all,

There are several mentions of covariance/contravariance in the
Introduction to Programming in ATS, but I don’t recall anything else
about what makes one type a subtype of another. Is it just a matter of
predicates on sorts, so nat n is a subtype of int n? Or is it something
more complicated?

Thanks,
Shea

P.S. I am not sure which group is appropriate to post to.

3

Yes. When building an API in ATS for GTK, I had to capture the class
hierarchy of GTK inside the type system of ATS.On Saturday, August 30, 2014 12:32:47 AM UTC-4, Shea Levy wrote:

Ah, thanks! Are there ever cases where you have to prove some type a
subtype of another?

~Shea

On Fri, Aug 29, 2014 at 03:00:28PM -0700, gmhwxi wrote:

It is just a matter of predicates on type indices.

Assume:

typedef Pos = [a:int | a > 0] int(a)
typedef Nat = [a:int | a >= 0] int(a)

Pos is a subtype of Nat since (a > 0) implies (a >= 0)

Also, there are some built-in subtyping relations. For instance,

int(n) is a subtype of int (un-indexed); bool(b) is a subtype of
bool (un-indexed); etc.

On Friday, August 29, 2014 5:25:23 PM UTC-4, Shea Levy wrote:

Hi all,

There are several mentions of covariance/contravariance in the
Introduction to Programming in ATS, but I don’t recall anything else
about what makes one type a subtype of another. Is it just a matter of
predicates on sorts, so nat n is a subtype of int n? Or is it
something
more complicated?

Thanks,
Shea

P.S. I am not sure which group is appropriate to post to.

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/7ecdbbfc-e171-4926-84ad-4051d603f81d%40googlegroups.com.

4

The list0 example in the FAQ may also be interesting:

Brandon Barker
brandon…@gmail.comOn Fri, Aug 29, 2014 at 6:00 PM, gmhwxi gmh...@gmail.com wrote:

It is just a matter of predicates on type indices.

Assume:

typedef Pos = [a:int | a > 0] int(a)
typedef Nat = [a:int | a >= 0] int(a)

Pos is a subtype of Nat since (a > 0) implies (a >= 0)

Also, there are some built-in subtyping relations. For instance,

int(n) is a subtype of int (un-indexed); bool(b) is a subtype of
bool (un-indexed); etc.

On Friday, August 29, 2014 5:25:23 PM UTC-4, Shea Levy wrote:

Hi all,

There are several mentions of covariance/contravariance in the
Introduction to Programming in ATS, but I don’t recall anything else
about what makes one type a subtype of another. Is it just a matter of
predicates on sorts, so nat n is a subtype of int n? Or is it something
more complicated?

Thanks,
Shea

P.S. I am not sure which group is appropriate to post to.

–
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/7ecdbbfc-e171-4926-84ad-4051d603f81d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/7ecdbbfc-e171-4926-84ad-4051d603f81d%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

Ah, thanks! Are there ever cases where you have to prove some type a
subtype of another?

~SheaOn Fri, Aug 29, 2014 at 03:00:28PM -0700, gmhwxi wrote:

It is just a matter of predicates on type indices.

Assume:

typedef Pos = [a:int | a > 0] int(a)
typedef Nat = [a:int | a >= 0] int(a)

Pos is a subtype of Nat since (a > 0) implies (a >= 0)

Also, there are some built-in subtyping relations. For instance,

int(n) is a subtype of int (un-indexed); bool(b) is a subtype of
bool (un-indexed); etc.

On Friday, August 29, 2014 5:25:23 PM UTC-4, Shea Levy wrote:

Hi all,

There are several mentions of covariance/contravariance in the
Introduction to Programming in ATS, but I don’t recall anything else
about what makes one type a subtype of another. Is it just a matter of
predicates on sorts, so nat n is a subtype of int n? Or is it something
more complicated?

Thanks,
Shea

P.S. I am not sure which group is appropriate to post to.

–
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/7ecdbbfc-e171-4926-84ad-4051d603f81d%40googlegroups.com.