Indexed-type vs dependent-type

[Yannick Duchêne]

There was a thread, I can't remember which one, with a suggestion to use `string` instead of `String` as `String` is a dependent type and `string` is not, so `string` would be more simple for the intended use. Today I used something of the form `string(n)` and so I was surprised to read this comment. Then I saw `string` is an alias of `string_int_type`, which explicitly has an index: `string_int_type (n: int) = string_type`.

Before mid-day of today, both was the same in my mind.

Is the difference in quantifiers? `string_int_type` is not dependent because there is no quantifier as there is one in `typedef String = [n:int] string_int_type (n)`? That said, what this quantifier do here, is unclear to me, as there is no associated predicate.

May be should I ask to be sure, about another assumption I have in my mind, in case it's wrong: an indexed type is one partition among the possible values of its base type, isn't it?

[gmhwxi]

'string' is overloaded:

stadef string = string_type // non-indexed
stadef string = string_int_type // indexed

typedef String = [n:int] string(n)

String and string_type classify the same set of values.

When implementing type-checking, one is constantly concerned with
type equality: how to tell whether two types are the same.

String is not algebraic (as it contains a quantifier). In general, type equality on
non-algebraic types (that is, those using quantification) is difficult. Also, non-algebraic
types cannot be directly used as template parameters. This is why string_int is preferred
over String.

g1ofg0_string allows one to go from String to string_type. Many such functions overload
the symbol g1ofg0. For instance, one often sees the following kind of code in the library of ATS:

val str = g1ofg0(str) // str: string changes into String

[Yannick Duchêne]

Le mercredi 13 mai 2015 03:25:20 UTC+2, gmhwxi a écrit :

String is not algebraic (as it contains a quantifier). In general, type equality on
non-algebraic types (that is, those using quantification) is difficult. Also, non-algebraic
types cannot be directly used as template parameters. This is why string_int is preferred
over String.

So about the other question, is it right to say a dependent type is an indexed non-algebraic type? I wonder about it to to help understand what may be read at other places. And is it right to say an indexed type is one partition of a base type? (or the single partition, if ever any base type can have one only indexed form)

And what's the effect of an existential quantifier (as with String) with no predicate?

[gmhwxi]

The notion of dependent types is like this:

Say there is a dynamic integer value x. We can form a type string(x)
for strings whose length is x. The type string(x) is a dependent type
as its meaning depends on x, a dynamic integer.

The dependent types in ATS are a bit different. 'string(x)' cannot be formed
in ATS as x is not static. However, we can form 'string(n)' for a static integer
n such that x is of the type int(n). As int(n) is a singleton type, x and n have the
same value. The dependent types in ATS are often referred as indexed types
or DML-style dependent types (as they originates from DML).

>>an indexed type is one partition of a base type

It may not necessarily be a partition. For instance, we can also interpret string(n)
as the type for string of length less than n. Then string(1) and string(2) overlap.

We often use the word 'refinement': string(n) is a refinement of string as it gives
out more information.

[Yannick Duchêne]

This message is wished to be for documentation purpose, not really a question (although comments from anyone are always welcome). In the while, two common error messages from ATS may be made clear, with simple samples.

Say one want to define a Positive type, à la Ada, that is a Natural greater than zero (used for human intuitive array indexes, as an example). This may be achieve in two ways, and the combination of two ways, also show the usefulness of overloadable static definition, as discussed in https://groups.google.com/d/msg/ats-lang-users/oCr35CMrIr0/_mNmVfNyPiEJ .

The first way, which may be the most obvious is to constrain the type's allowed value:

typedef pos = [n: nat | n >= 1] int(n) // Declaration #1

However, this won't allow to use the `pos` type as one may do when using `string(n)`. This may be achieved with this variant:

typedef pos(n: int) = [n >= 1] int(n)  //Declaration #2

Now here, to check what follows, one will need to comment-out either declaration #1 or #2 to only keep the one tested.

Say one have only declaration #1 (and not #2), then one may have:

val a: pos = 1

However, if one do this…

val a: pos(1) = 1

…he/she will get a famous ATS error message, “the static term is overly applied”, and the meaning seems obvious here: it means the type of `a` is over‑specified, an attempt to specify it beyond what the `pos` type defines.

Now commenting‑out declaration #1 and keeping declaration #2 alone, one may have next to it:

val a: pos(1) = 1

However, if one try to have the former `val` declaration instead, that is…

val a: pos = 1

…he/she will get another famous ATS error message: “[…] expression needs to be impredicative […]”. In this context, it's obvious it's the contrary of the former error message, it's not an over‑specification, it's a lack of a required specification (for the meaning of `pos` here to make sense).

Now getting both declaration #1 and #2 together, that is…

typedef pos = [n: nat | n >= 1] int(n)
typedef pos(n: int) = [n >= 1] int(n)

…one may have both:

val a: pos = 1
val a: pos(1) = 1

…together, thanks to `stadef`/`typedef` declaration being overloadable (as explained in https://groups.google.com/d/msg/ats-lang-users/oCr35CMrIr0/_mNmVfNyPiEJ )

To go further, one may noticed there is a relation between declaration declaration #1 and declaration #2, and wish this relation could be expressed in some way. At least this can be achieved using a `sortdef` (not sure it's the right way to do, though):

sortdef pos = {n: nat | n >= 1}

The previous constraint may be rewritten, so the previous…

typedef pos = [n: nat | n >= 1] int(n)
typedef pos(n: int) = [n >= 1] int(n)

…may be rewritten as:

typedef pos = [n: pos] int(n)
typedef pos(n: int) = [p: pos | n == p] int(p)

The first is rather obvious (still note how the sort can have the same name as the types), the second deserves two practical comments.

The first comment is the use of `==` instead of `=` which (a reminder) stands for the equality in the statics of ATS (`==` for equality between static values, `=` for equality between dynamic values… there are other operators with similar status).

The second comment is about how the constraint is passed to `int`…

First trying this, which is not the same as the above…

typedef pos(n: int) = [p: pos | n == p] int(n)
val a: pos(1) = 1

… one will get an “unsolved constraint” error.

So this really has to be `p` and not `n` which is to be used, although the constraint says `n == p` (I have to admit the reason remains mysterious to me, why only one match the intent):

typedef pos(n: int) = [p: pos | n == p] int(p)
val a: pos(1) = 1

Now one have…

sortdef pos = {n: nat | n >= 1}
typedef pos = [n: pos] int(n)
typedef pos(n: int) = [p: pos | n == p] int(p)

…which allows both…

val a: pos = 1

…and…

val a: pos(1) = 1

…together, and with an explicit relation between the two `typedef` declarations, via a prior `sortdef` to express the common constraint, which is `{n: nat | n >= 1}`.

(with the hope there aren't too much error or mistake left in this message)

[Yannick Duchêne]

Le mercredi 13 mai 2015 06:11:24 UTC+2, gmhwxi a écrit :

The dependent types in ATS are a bit different. 'string(x)' cannot be formed
in ATS as x is not static. However, we can form 'string(n)' for a static integer
n such that x is of the type int(n). As int(n) is a singleton type, x and n have the
same value. The dependent types in ATS are often referred as indexed types
or DML-style dependent types (as they originates from DML).

About this kind of declaration, I just had a surprise, and wonder about index on abstype and index on type, or if I understand one as an index as explained while it is not.

While trying to express something in different ways, I wanted to check if some expressions would type-check (to check it really means what was intended), and I came to test something like this:

sortdef i = int
abstype t
typedef t(i: i) = t

extern fun t(): t(1)
extern fun f(a: t(1)): bool
val b = f(t(): t(2)) // Oops… does not fail.

Surprisingly, it passes type-checking.

Changing `typedef` into `abstype` on the third line, it does not type-check (and that's OK, that's what I was initially expecting).

sortdef i = int
abstype t
abstype t(i: i) = t

extern fun t(): t(1)
extern fun f(a: t(1)): bool
val b = f(t(): t(2)) // Fails with constraint error: OK.

What does `typedef t(i: i) = t` really means ? Seems it does not mean what I though.

Another syntax and meaning issue, is with this:

sortdef i = int
abstype t
typedef t(i: i) (* sort with index name *) = t

extern fun t(): t(1)

ATS accepts the above, but not the next:

sortdef i = int
abstype t
typedef t(i) (* sort alone, without index name *) = t

extern fun t(): t(1)

With this one, it complains “none of the static constants referred to by [t] is applicable”. But it's an int sort which is specified, or not?

When `typedef` is changed into `abstype` on the third line, ATS accepts `t(1)` with both `abstype t(i: i) = t` and `abstype t(i) = t`.

What's the real meaning of these declarations?

[gmhwxi]

If you do

typedef t(i:int) = t // transparent

then the typechecker knows that t(i) = t for all integers i.

If you do

abstype t(i:int) = t // opaque

then the typechecker does not know that t(i) = t. This information
is only used later by the compiler for code generation.

[gmhwxi]

If you write

typedef t(i) = t,

then 'i' is assumed to be a variable (not a sort).

If you write

abstype t(i)

then 'i' is treated as a sort (not a variable).

[Yannick Duchêne]

OK, so the opacity of abstract type in ATS, goes beyond the traditional hiding of implementation, with ex. opaque records, hidden attributes and the like, it's a part of the type derivation which is hidden.

That's clearer.

[Yannick Duchêne]

Le jeudi 14 mai 2015 21:36:25 UTC+2, gmhwxi a écrit :

If you write

typedef t(i) = t,

then 'i' is assumed to be a variable (not a sort).

If you write

abstype t(i)

then 'i' is treated as a sort (not a variable).

A variable of a default sort, Professor?

Once again, thanks for your pleasant answers.

[Hongwei Xi]

If you do

abst@ype foo = bar

the compiler only assumes that foo and bar uses the same layout.

On Thu, May 14, 2015 at 3:45 PM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:

OK, so the opacity of abstract type in ATS, goes beyond the traditional hiding of implementation, with ex. opaque records, hidden attributes and the like, it's a part of the type derivation which is hidden.

That's clearer.

Le jeudi 14 mai 2015 21:34:17 UTC+2, gmhwxi a écrit :

--
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/2b3074b8-064e-4d56-8cca-106b2d93cb08%40googlegroups.com.

[Hongwei Xi]

>>A variable of a default sort, Professor?

A variable of a sort that can only be determined when

t(...) is used for the first-time. I suggest that this feature be

avoided.

--
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/53a6f964-3f8b-4fcb-9c1c-0e7b3f74f6af%40googlegroups.com.