# Indexed-type vs dependent-type

**URL:** <https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473>\
**Category:** Google Group\
**Created:** [May 13, 2015, 12:18am UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473 "2015-05-13T00:18:53Z")\
**Posts on this page:** 12\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 13, 2015, 12:18am UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/1 "2015-05-13T00:18:53Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 13, 2015, 4:48pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/2 "2015-05-13T16:48:50Z")

</div>

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](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](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)Le mercredi 13 mai 2015 06:11:24 UTC+2, gmhwxi a écrit :

> 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.
> 
> On Tuesday, May 12, 2015 at 11:57:11 PM UTC-4, Yannick Duchêne wrote:
> 
> > 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?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 14, 2015, 7:34pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/3 "2015-05-14T19:34:17Z")

</div>

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.On Thursday, May 14, 2015 at 3:13:29 PM UTC-4, Yannick Duchêne wrote:

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 14, 2015, 7:47pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/4 "2015-05-14T19:47:30Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 13, 2015, 3:57am UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/5 "2015-05-13T03:57:11Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 14, 2015, 7:52pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/6 "2015-05-14T19:52:34Z")

</div>

> > 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.On Thu, May 14, 2015 at 3:47 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> 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.
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/53a6f964-3f8b-4fcb-9c1c-0e7b3f74f6af%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/53a6f964-3f8b-4fcb-9c1c-0e7b3f74f6af%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/53a6f964-3f8b-4fcb-9c1c-0e7b3f74f6af%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 13, 2015, 4:11am UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/7 "2015-05-13T04:11:24Z")

</div>

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.On Tuesday, May 12, 2015 at 11:57:11 PM UTC-4, Yannick Duchêne wrote:

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 13, 2015, 1:25am UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/8 "2015-05-13T01:25:20Z")

</div>

‘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 StringOn Tuesday, May 12, 2015 at 8:18:53 PM UTC-4, Yannick Duchêne wrote:

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 14, 2015, 7:50pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/9 "2015-05-14T19:50:17Z")

</div>

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](mailto: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 :
> 
> > 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.
> > 
> > On Thursday, May 14, 2015 at 3:13:29 PM UTC-4, Yannick Duchêne wrote:
> > 
> > > 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?
> > 
> > –  
> > 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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/2b3074b8-064e-4d56-8cca-106b2d93cb08%40googlegroups.com)  
> > [https://groups.google.com/d/msgid/ats-lang-users/2b3074b8-064e-4d56-8cca-106b2d93cb08%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/2b3074b8-064e-4d56-8cca-106b2d93cb08%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 14, 2015, 7:36pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/10 "2015-05-14T19:36:25Z")

</div>

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).On Thursday, May 14, 2015 at 3:13:29 PM UTC-4, Yannick Duchêne wrote:

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 14, 2015, 7:13pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/11 "2015-05-14T19:13:29Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 14, 2015, 7:46pm UTC](https://discourse.ats-lang.org/t/indexed-type-vs-dependent-type/473/12 "2015-05-14T19:46:11Z")

</div>

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 :

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