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

------