###### # # 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] ######