Subtyping?

[Shea Levy]

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.

[gmhwxi]

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.

[Brandon Barker]

The list0 example in the FAQ may also be interesting: https://github.com/githwxi/ATS-Postiats/wiki/Frequently-asked-questions#i-have-two-different-types-being-used-together-in-the-same-data-structure-and-they-typecheck-is-this-a-bug

Brandon Barker
brandon...@gmail.com

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

[Shea Levy]

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

~Shea

[gmhwxi]

Yes. When building an API in ATS for GTK, I had to capture the class
hierarchy of GTK inside the type system of ATS.