Frequently Asked Questions:
------
Q. What is the difference between sorts and extended sorts?
A. The statics of ATS is typed and the types for static terms are called
sorts. An extended sort is either a sort or a subset sort. For instance,
[int] is a sort and [nat] is a subset sort defined as follows
sortdef nat = {a:int | a >= 0}
The only use of extended sorts is to form types. For instance, we can
form a type as follows
{a:t@ype} {n:,i:nat | i < n} (array (a, n), int i) -> a
which is considered a shorthand for the type below:
{a:t@ype} {n,i:int | 0 <= i; i < n} (array (a, n), int i) -> a
However, the following is a typical erroneous use of subset sorts:
datatype list (t@ype+, nat) = ...
^^^
Instead, the sort [int] needs to chosen to replace the sort [nat]. In
order to capture the fact that all lists have nonnegative length, one
may introduce a type definition as follows:
type list' (a:t@ype, n:int) = [n >= 0] list (a, n)
------
Q. What is the difference between props and types?
A. In ATS, props are assigned to proofs and types are assigned to
programs. While proofs are required to be pure and total, programs can
be and often are effectful and partial.
------
Q. What are the differences among [case], [case-] and [case+]?
A. [case+] requires that pattern matching be exhaustive. If pattern
matching is not exhaustive, then an *error* message is issued. On the
other hand, [case] only requires that a *warning* message be issued if
pattern matching is not exhaustive. For [case-], no exhaustiveness test
is performed. The use of [case-] is recommended only when the code is
generated automatically via some tools (e.g., atsyacc).
Note that pattern matching must be exhaustive in (valid) proofs, thus
the use of [case+] is mandatory if a case-expression needs to be formed
during proof construction.
------
Q. What are the differences among [val], [val+], [val-]?
A. The differences are parallel to those among [case], [case+] and [case-].
------
Q. What do {..} and {...} stand for?
A. In the case where a value is passed whose type begins with universal
quantifiers, one may need to instantiate these quantifers first before
passing the value. The syntax {..} acts like a marker to inform the
type-checker that one instantiation is needed here. In order to
eliminate all quantifiers, {...} needs to be used. Note that in most
cases such markers can be automatically inferred and thus need not to be
supplied explicitly by the programmer.
------
Q. What is the difference between [C] and [C()], where [C] is a value
constructor (associated with a datatype) of arity 0.
A. [C] and [C()] are really the same when used as expressions. However,
as patterns, [C] and [C()] are completely different: the former is
treated as a variable pattern while the latter only matches the value
[C()]. For instance, the following program will be rejected as the
second clause is redundant (since [nil] is a variable pattern that
matches anything):
fun isEmpty {a:t@ype} (xs: list (a, n)): bool (n == 0) =
case+ xs of
| nil => true
| cons _ => false
Instead, the problem can be fixed as follows:
fun isEmpty {a:t@ype} (xs: list (a, n)): bool (n == 0) =
case xs of
| nil () => true // using [nil _] for [nil ()] is fine, too
| cons _ => false
------