######
#
# 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 universally or existentially
quantified 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 | n >= 0; i >= 0; 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 be 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:
typedef list' (a:t@ype, n:int) = [n >= 0] list (a, n)
A definition as such , however, does not seem particularly useful in
practice.
------
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.
------
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 of arity 0 (that is associated with some datatype).
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 is 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
// end of [isEmpty]
Instead, the problem, which is quite common for beginners programming in
ATS, can be easily 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
// end of [isEmpty]
------
Q. What is the difference between the following two forms of type annoation:
1. let val x : T = e in ... end
2. let val x = e : T in ... end
A. In the first case, the type of [e] must be synthesized and this type is
then compared with the type T. If type synthesis fails, a type error is
reported.
In the second case, the type of the expression [e : T] is [T], which is
immediately assigned to [x], and [e] is then checked against [T].
If in doublt, please choose the second form of type annotation.
------
Q. What is the symbol for "not equal"?
A. The symbol "<>" is used for "not equal".
------
Q. How to write a single precision float point number in ATS?
A. Each of the following expressions gives a single precision float point
number representing 3.1415926:
3.1415926f
(3.1415926: float)
float_of_double(3.1415926)
------
Q. What is the difference between the following declarations:
fun id1 {a:type} (x: a): a = x // [a] is a boxed type
fun{a:t@ype} id2 (x: a): a = x // [a] is of unknown size
A. [id1] is a polymorphic function in ATS, and it can be type-checked and
compiled. However, [id1] can only be applied to a value of some boxed
type. [id2] is a function template in ATS, and it can be type-checked
but not compiled immediately. Just like function templates in C++, only
instances of [id2] are compiled. If one defined a polymorphic function
as follows:
fun id3 {a:t@ype} (x:a ): a = x // [a] is of unknown size
then this function can be type-checked and compiled. However, the C code
generated from this function contains a type (ats_abs_type) of unknown size,
and it results in some error when further compiled by a C compiler. Thus,
[id3] cannot really be used in practice.
------
###### end of [FAQ.txt] ######