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