Changeset a03ed29 for doc

Timestamp:

Jul 24, 2024, 7:11:32 PM (6 months ago)

Author:

JiadaL <j82liang@…>

Branches:

master

Children:

5aeb1a9

Parents:

e561551 (diff), b6923b17 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

conclude merge

Location:

doc

Files:

• LaTeXmacros/lstlang.sty (modified) (2 diffs)
• proposals/iterators.md (modified) (2 diffs)
• theses/fangren_yu_MMath/content1.tex (modified) (1 diff)
• theses/fangren_yu_MMath/content2.tex (modified) (1 diff)
• theses/fangren_yu_MMath/performance.tex (modified) (1 diff)
• theses/jiada_liang_MMath/CFAenum.tex (modified) (7 diffs)
• theses/jiada_liang_MMath/background.tex (modified) (8 diffs)
• theses/jiada_liang_MMath/implementation.tex (modified) (1 diff)
• theses/jiada_liang_MMath/intro.tex (modified) (5 diffs)

doc/LaTeXmacros/lstlang.sty

@@ -8 +8 @@
 %% Created On       : Sat May 13 16:34:42 2017
 %% Last Modified By : Peter A. Buhr
-%% Last Modified On : Fri May 31 14:36:02 2024
-%% Update Count     : 44
+%% Last Modified On : Wed Jul 24 07:40:11 2024
+%% Update Count     : 45
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -115 +115 @@
         morekeywords={
                 alignas, _Alignas, alignof, _Alignof, __alignof, __alignof__, and, asm, __asm, __asm__, _Atomic, __attribute, __attribute__,
-                __auto_type, basetypeof, _Bool, bool, catch, catchResume, choose, coerce, corun, cofor, _Complex, __complex, __complex__,
+                __auto_type, basetypeof, _Bool, bool, catch, catchResume, choose, coerce, cofor, corun, countof, _Complex, __complex, __complex__,
                 __const, __const__, continue, coroutine, _Decimal32, _Decimal64, _Decimal128, disable, dtype, enable, exception, __extension__,
                 fallthrough, fallthru, finally, fixup, __float80, float80, __float128, float128, _Float16, _Float32, _Float32x, _Float64,

doc/proposals/iterators.md

@@ -10 +10 @@
 There are two groups of types that interact with this proposal.
 
+Iterable
+
+An iterable is a container of some type that has a default iterator that goes
+over its own contents. It may be a logical container, like a mathematical range,
+that does not store elements in memory, but it should have logical elements.
+A trait is defined to standardize how to get that iterator.
+
+        forall(C, I)
+        trait is_iterable {
+                I get_iterator(C&);
+        }
+
+This is not particularly useful on its own, but is used as standardized glue
+between some other features below.
+
 Iterator
 
-An iterator has a very simple interface with a single operation.
-The operation is "get the next value in the sequence", but this actually has
-several parts, in that it has to check if there are move values, return the
-next one if there is one, and update any internal information in the iterator.
-For example: `Maybe(Item) next(Iter &);`.
-
-Now, iterators can have other operations. Notably, they are often also
-iterables that return themselves. They can also have a verity of iterator
-transformers built in.
-
-Iterable
-
-Anything that you can get an iterator from is called an iterable. There
-is an operation to get an iterator from an iterable.
-
-Range For Loop
---------------
-One part of the language that could be reworked to make good use of this is
-for loops. In short, remove most of the special rules that can be done inside
-the identifier and make it a generic range for loop:
-
-    ```
-    for ( IDENTIFIER ; EXPRESSION ) STATEMENT
-    ```
-
-The common way to implement this is that expression produces an iterable.
-The for loop gets an iterator from the iterable (which is why iterators are
-often iterables, so they can be passed in with the same interface) and stores
-it. Then, for each value in the iterator, the loop binds the value to the
-identifier and then executes the statement. The loop exits after every value
-has been used and the iterator is exhausted.
-
-For the chained for loop (`for (i; _: j; _)`) can still have its existing
-behaviour, advancing through each range in parallel and stopping as soon
-as the first one is exhausted.
+An iterator is an object that can be advanced through a sequence of values.
+An iterator can be checked to see if it is at the end of the sequence, if not
+the next value can be retrieved from it and the iterator advanced. This can
+be done in as little as a single operation:
+
+        forall(Iter, Elem)
+        trait is_iterator {
+                maybe(Elem) next(Iter&);
+
+                // is_iterable(I, I&)
+                Iter& get_iterator(Iter&);
+        }
+
+This interface is not fixed, the function could change or be split into
+multiple functions (ex: `bool next(Elem&, Iter&)`). It should be natural,
+but also efficient to implement. This version will be used for examples in
+the proposal.
+
+When next is called, if there are elements left in the iterators, the next
+element is returned in a maybe and the iterator is advanced. If the iterator
+is exhausted nothing is changed and an empty maybe is returned.
+
+Iterators are also iterables. They must return themselves, this allows
+iterators to be used directly where iterables are expected.
+
+For-Each Loop
+-------------
+The main part of this proposal which is part of the language definition,
+the rest is part of the standard library. And this is the new for-each loop:
+
+        for ( IDENTIFIER ; EXPRESSION ) STATEMENT
+
+While this uses similar syntax to the existing special for loops, but takes
+a standard expression. This expression is evaluated, and then the iterator is
+retrieved from it (this should be the identity function iterators). Each
+iteration of the loop then checks the iterator to see if it is exhausted, if
+not it uses the value to execute the statement. If the iterator is exhausted,
+the loop is completed, and control continues after the loop (or the else
+clause if provided).
+
+The loop should show the same behaviour as the following code:
+(`typeof(?)` should be decided by the resolver.)
+
+        {
+                typeof(?) __iterable = EXPRESSION;
+                typeof(?) __iterator = get_iterator(__iterable);
+                typeof(?) __next = next(__iterator);
+                while (has_value(&__next)) {
+                        typeof(?) IDENTIFIER = get(&__next)
+                        STATEMENT
+                        __next = next(__iterator);
+                }
+        }
+
+This new loop can (but may not need to) also support the existing variants,
+where the name is omitted or multiple iterators are advanced in lock-step:
+
+        for ( EXPRESSION ) STATEMENT
+        for ( IDENTIFIER0 ; EXPRESSION0 : IDENTIFIER1 ; EXPRESSION1 ) STATEMENT
+
+These may not be needed. The unnamed variant is a nice short hand.
+The multiple iterator method could be replaced with an iterator transformer
+that has the same behaviour:
+
+        for (i, j, k; zip(iter, range, container)) { ... }
+
+This would require some further extensions, but would also allow single
+iterators to iterate over sets of related values. It also shows how library
+features can be used to extend the for-each loop.
+
+Containers as Iterables
+-----------------------
+The primary iterator application is going over the contents of various
+collections. Most of the collections should support the iterable interface.
+Each of these iterators should go over each element in the container.
+
+They could support multiple iterator interfaces. For example, a map could go
+over key-value-pairs, or just keys or just values.
+
+There isn't a lot to say here, except that as the implementation progresses,
+various rules about iterator invalidation should be hammered out.
 
 Ranges
 ------
-Ranges, which may be a data type or a trait, are containers that contain
-a sequence of values. Unlike an array or vector, these values are stored
-logically instead of by copy.
-
-The purpose of this container is to bridge the new iterator interfaces with
-the existing range syntax. The range syntax would become an operator that
-returns a range object, which can be used as any other type.
-
-It might not cover every single case with the same syntax (the `@` syntax may
-not translate to operators very well), but should be able to maintain every
-option with some library range.
-
-Library Enhancements
---------------------
-There are various other tools in the library that should be improved.
-The simplest is to make sure most containers are iterables.
-
-Also, new utilities for manipulating iterators should be created. The exact
-list would have to wait but here are some examples.
-
-Transformers take in an iterator and produce another iterator.
-Examples include map, which modifies each element in turn, and filter,
-which checks each element and removes the ones that fail.
-
-Producers create new iterators from other information.
-Most practical iterators tend to be iterable containers, which produce all
-the elements in the container, this includes ranges. Others include infinite
-series of one element.
-
-Consumers take an iterator and convert it into something else.
-They might be converted into a container or used in a for loop. Dedicated
-consumers will be some form of folding function.
+The existing range syntax is incompatible with the for-each loop. But this
+can be recovered by making at least some of the range syntax into operators.
+These operators create and return new range types.
+
+The ranges are types that map a random numeric range. For iteration, a range
+is also considered an iterator over the numbers in the range.
+
+The there could be up to 6 new operators to create ranges. These are:
+    `~` `+~` `~=` `+~=` `-~` `-~=`
+
+Parsing issues might rule some of these out. Others may be rendered
+irrelevant by iterator transformers. For example, adding a transformer that
+reverses the iterator could replace having downwards range operators.
+
+The one range that does not involve the operator is the lone number. This is
+a shorthand for a half-open/exclusive range from zero to the given number.
+That is the same behaviour as one (or two ~ and +~) of the existing range
+operators. So it only saves 2-3 characters.
+
+But if we want to save those characters, there may be a special form that
+could be used (for example, in the unnamed case) or you could treat integers
+as iterables that create iterators that count from zero up to the limit.
+
+        forall(N) struct Upto { N current; N limit; };
+        Upto(int) get_iterator(const int&);
+
+Enumerations as Iterators
+-------------------------
+To convert enumerations to the new form, a new syntax will have to be created
+to treat an enumeration type as an expression returning a range.
+
+Using the unmodified type name seems problematic, it could be done if we
+convert the type expression to some type object that can be passed to the
+get_iterator function. But there are other alternatives.
+
+An operator could be created to convert the type into an iterable expression.
+
+        range_over(EnumType)
+
+It is also possible to create a library type that iterates over the range.
+Then we use a compound literal of a nullary type as a flag to get it.
+
+        (ERange(EnumType)){}
+
+Both of these are placed in the EXPRESSION part of the for-each loop.
+
+Iterator Transformers
+---------------------
+New library features could be created to work with iterators. One of the
+biggest groups are transformers, which allow for more complicated compound
+operations on iterators.
+
+For a few examples:
+
+        // Create a new iterator that transforms elements from a source iterator.
+        forall(I, T, U | is_iterator(I, T))
+        /* Iterator over U */ map(U (*func)(T), I iter);
+
+        // Create an iterator that keeps only elements that satisfy a predicate.
+        forall(I, T | is_iterator(I, T))
+        /* Iterator over T */ filter(bool (*pred)(const T&), I iter);
+
+        forall(Is..., Ts... | is_iterator(Is, Ts)...)
+        /* Iterator over [Ts] */ zip(Is iters);
+
+        forall(Index, I, T | is_serial(Index) | is_iterator(I, T))
+        /* Iterator over [Index, T]) */ enumerate(Index, I);
+
+The return type is omitted in each case, because usually these functions end
+up being thin wrappers around a constructor for a specialized type that is
+the iterator, in each case, this is the return type.
+
+Also, these should be over iterables (with the conversion from iterable to
+iterator part of the thin wrapper), not just iterators. But the examples are
+easier to write out this way.
+
+Here is one example expanded to cover those details:
+
+        forall(Iter, Elem)
+        struct Filter {
+                bool (*pred)(const Elem&);
+                Iter iterator;
+        }
+
+        forall(Iter, Elem | is_iterator(Iter, Elem))
+        maybe(Elem) next(Filter(Iter, Elem) & this) {
+                maybe(Elem) ret;
+                do {
+                        ret = next(this.iterator);
+                } while (has_value(ret) && this.pred(get(&ret)));
+                return ret;
+        }
+
+        forall(T, Iter, Elem | is_iterable(T, Iter) | is_iterator(Iter, Elem))
+        Filter(Iter, Elem) filter(bool (*pred)(const Elem&), T& iterable) {
+                return (Filter(Iter, Elem)){ pred, get_iterator(iterable) };
+        }
+
+Iterator Consumers
+------------------
+Eventually we will have to turn the iterators into something else. Iterator
+consumers take an iterator and turn it into something else. The biggest of
+these is the for-each loop, as described above. In addition various library
+functions can be added.
+
+One group of functions are container constructors which take everything from
+the iterable and build a new container out of it. There would be various
+instances of this because you will need one for each container type.
+
+Higher order folding functions (for example, the functional
+`foldr : (a -> b -> b) -> b -> [a]`) are a bit less useful since Cforall does
+not work with anonymous functions quite as well. However, some of the
+specialized versions may still be useful. For example, getting the sum of an
+iterable's elements.
+
+        forall(T, I, N | is_iterable(T, I) | is_iterator(I, N) |
+                        { void ?{}(N&, zero_t); N ?+=?(N&, N); })
+        N sum(T & iterable) {
+                N acc = 0;
+                for ( i ; iterable ) acc += i;
+                return acc;
+        }
+
+Iterator Producers
+------------------
+Another group of library features are iterator producers, that take some
+data and create an iterator out of it. Many of already discussed cases are
+actually examples of this (containers, ranges and enumerations).
+
+There are a few more cases that might be useful. Such as "repeat", which
+takes a single element and iterates over it infinitely. This is usually
+combined with other iterators and not used directly.
+
+Other Improvements to Cforall
+----------------------------
+All code snippets should be considered pseudo-code because they require some
+features that do not currently exist. There are also some that just run into
+current bugs. For instance, my proof of concept for ERange encountered a few
+warnings even after I got it working.
+
+This proposal might also benefit from associated types. Both is_iterable and
+is_iterator may not need to be generic over all their type parameters.
+
+Tuple enhancements might also help with iterators that want to return more
+than one value.
 
 Related Work
 ------------
-Python has a robust iterator tool set. It also has a `range` built-in which
-does many of the same things as the special for loops (the finite and
-half-open ranges).
+Python has a robust iterator tool set. It uses the same iterator / iterable
+divide as described above and has the interfaces (note, Python uses duck
+typing instead of defined interfaces, so these are "imaginary"):
+
+        class Iterable:
+
+                def __iter__(self):
+                        # Return an iterator over the iterable's contents.
+
+        class Iterator(Iterable):
+
+                def __iter__(self):
+                        # Iterators are iterable over themselves.
+                        return self
+
+                def __next__(self):
+                        # Return next value if present and advance internal state.
+                        # Otherwise raise StopIteration exception.
+
+It uses this in for loops, the for loop takes an iterable gets the iterable,
+and iterates until the iterable is exhausted. Iterators are iterables so they
+can be passed in directly as well.
+
+It also has a `range` built-in which handles integer loops, although only
+increasing half-open ranges.
 
 In addition, it has many dedicated iterator constructors and transformers,
 and many containers can both produce and be constructed from iterators.
-
+For example, the chain function goes though a series of iterators in sequence
+an can be used by:
+
+        import itertools
+        itertools.chain(iter_a, iter_b)
+
+Python enumerations are implemented in the standard library and are iterables
+over all their possible values. There is no special construct for this, in
+Python types are object, and the type of an enum type object is EnumType
+which supports the iterable interface.
+
+        for elem in SomeEnum:
+                print(elem)
+
+Python References
 +   https://docs.python.org/3/reference/datamodel.html#object.__iter__
 +   https://docs.python.org/3/library/functions.html#func-range
++   https://docs.python.org/3/library/enum.html
 
 C++ has many iterator tools at well, except for the fact it's "iterators" are
@@ -104 +315 @@
 They do appear to be a wrapper around the "pointer" iterators.
 
+        template< class T >
+        concept range = requires( T& t ) {
+                ranges::begin(t);
+                ranges::end(t);
+        };
+
+C++ also has "structured bindings" which can be used to unpack an object and
+bind its components to different names. This can be used to iterate over
+multiple values simultaneously. In this example from the Cforall compiler
+using a custom utility function written without special support.
+
+        for ( auto const & [index, handler] : enumerate( terminate_handlers ) ) {
+                ...
+        }
+
+C++ References
 +   https://en.cppreference.com/w/cpp/ranges
++   https://en.cppreference.com/w/cpp/language/structured_binding
 
 Rust also has a imperative implementation of a functional style of iterators,
+with iterator tools implemented as "Provided Methods". Provided methods
 including a great number of standard transformers. Otherwise, it is very
 similar to Python.
 
-+   https://doc.rust-lang.org/std/iter/index.html
+        pub trait Iterator {
+                type Item;
+
+                fn next(&mut self) -> Option<Self::Item>;
+
+                // Many provided methods ...
+        }
+
+Not that Rust has many of its iterator transformers stored as methods on the
+iterator. These methods are "provided" so you only have to define next, but
+you can redefine the other methods to provide optimizations.
+
+Rust also has range expressions. Based around `start .. end` and
+`start ..= end`, with the sub-expressions giving the start and end of the
+range being optional, except for end after `..=`. If start is omitted, the
+range has no lower bound, otherwise the range uses start as its inclusive
+lower bound. It is the same case for end and the upper bound, except that the
+`..=` will have an inclusive upper bound instead of an exclusive one.
+
+Rust achieves ordering and step control by iterator transformers. `.rev()`
+allows you to reverse a range and `.step_by(step)` provides a positive step
+value.
+
+Rust Reference
++   https://doc.rust-lang.org/std/iter/trait.Iterator.html
++   https://doc.rust-lang.org/reference/expressions/range-expr.html
++   https://doc.rust-lang.org/std/iter/trait.Iterator.html#method.rev

doc/theses/fangren_yu_MMath/content1.tex

@@ -1 @@
-\chapter{Content1}
+\chapter{Recent Features Introduced to \CFA}
 \label{c:content1}
 
-This chapter ...
-
-\section{Section 1}
-
-\section{Section 2}
+This chapter discusses some recent additions to the \CFA language and their interactions with the type system. 
+
+\section{Reference Types}
+
+Reference types are added to \CFA by Robert Schluntz in conjunction to his work on resource management. \CFA reference type is similar to \CC reference type but with its own added features. 
+
+The main difference between \CFA and \CC references is that \CC references are immutable, while \CFA supports reference rebinding operations. In \CC, references are mostly used in function parameters for pass-by-reference semantics, and in class members, which must be initialized during construction. Merely declaring a variable of reference type has little use as it only creates an alias of an existing variable. In contrast, \CFA reference variables can be reassigned (rebinded) and reference to reference is also allowed. 
+
+This example is taken from the feature demonstration page of \CFA: \footnote{Currently there are no plans of introducing \CC rvalue references to \CFA. Readers should not confuse the multi-reference declarations with \CC rvalue reference syntax.}
+
+\begin{cfa}
+int x = 1, y = 2, z = 3;
+int * p1 = &x, ** p2 = &p1,  *** p3 = &p2, // pointers to x
+        & r1 = x,  && r2 = r1,   &&& r3 = r2;  // references to x
+int * p4 = &z, & r4 = z;
+
+*p1 = 3; **p2 = 3; ***p3 = 3;                   // change x
+ r1 =  3;       r2 = 3;         r3 = 3;                 // change x: implicit dereference *r1, **r2, ***r3
+**p3 = &y;      *p3 = &p4;                                      // change p1, p2
+// cancel implicit dereferences (&*)**r3, (&(&*)*)*r3, &(&*)r4
+&r3 = &y; &&r3 = &&r4;                                  // change r1, r2
+\end{cfa}
+
+A different syntax is required for reassigning to a reference variable itself, since auto-deferencing is always performed and the expression \texttt{r1} would mean the \texttt{int} variable that \texttt{r1} referenced to instead. Using \CFA's reference types (including multi-references) we can actually describe the "lvalue" rules in C by types only, and the concept of lvalue could have been completely dropped off. However, since the cfa-cc program is not a full compiler but a transpiler from \CFA to C, lvalueness is still used in some places for code generation purposes, while the type checker now works on just types without needing to consider lvalueness of an expression.
+
+The current typing rules used in \CFA can be summarized as follows:
+
+\begin{enumerate}
+    \item For a variable x with declared type T, the variable-expression x has type reference to T, even if T itself is a reference type.
+    \item For an expression e with type $T\&_1...\&_n$ i.e. T followed by n references, where T is not a reference type, the expression \&T (address of T) has type T* followed by n-1 references.
+    \item For an expression e with type T* followed by n references, *T has type T followed by n+1 references. This is the reverse of previous rule, such that address-of and dereference operators are perfect inverses.
+    \item When matching parameter and argument types in a function call context, the number of references on the argument type is always stripped off to match the number of references on the parameter type \footnote{\CFA allows rvalue expressions be converted to reference values by implicitly creating a temporary variable, with some restrictions.}. In an assignment context, the left-hand side operand type is always reduced to a single reference.
+\end{enumerate}
+
+Under this ruleset, in a function call context, a type parameter will never be bound to a reference type. For example given the declarations
+
+\begin{cfa}
+    forall (T) void f (T&);
+
+    int &x;
+\end{cfa}
+
+The call f(x); will apply implicit dereference once to x so the call is typed f(int\&) with T=int, rather than with T=int\&.
+
+While initially the design of reference types in \CFA seeks to make it more like a "real" data type than reference in \CC, which mostly only serves the purpose of choosing argument-passing methods (by-value or by-reference) in function calls, the inherent ambiguity of auto-dereferencing still limits the behavior of reference types in \CFA polymorphic functions. Moreover, there is also some discrepancy of how the reference types are treated in initialization and assignment expressions. In the former case no implicit dereference is applied at all (see line 3 of example code) and in the latter case there is actually no assignment operators defined for reference types; the reassignment of reference variables uses the assignment operators for pointer types instead. There is also an annoying issue (although purely syntactic) that to pass in a null value for reference initialization one has to write \texttt{int \& r1 = *0p;} which looks like dereferencing a null pointer, but the dereferencing operation does not actually happen and the expression is eventually translated into initializing the underlying pointer value to null.
+
+This second point of difference would prevent the type system to treat reference types the same way as other types in many cases even if we allow type variables to be bound to reference types. This is because \CFA uses the common "object" trait (constructor, destructor and assignment operators) to handle passing dynamic concrete type arguments into polymorphic functions, and the reference types are handled differently in these contexts so they do not satisfy this common interface. 
+
+When generic types are introduced to \CFA, some thoughts had been put into allowing reference types as type arguments. While it is possible to write a declaration such as \texttt{vector(int\&)} for a container of reference variables, it will be disallowed in assertion checking if the generic type in question requires the object trait for the type argument (a fairly common use case) and even if the object trait can be made as non-required, the current type system often misbehaves by adding undesirable auto-dereference and operate on the referenced-to value rather than the reference variable itself as intended. Some tweaks would have to be made to accommodate reference types in polymorphic contexts and we are still not sure of what can or cannot be achieved. Currently we have to reside on using pointer types and giving up the benefits of auto-dereference operations on reference types.
+
+
+
+\section{Tuple Types}
+
+The addition of tuple types to \CFA can be traced back to the original design by David Till in K-W C, a predecessor project of \CFA. The introduction of tuples was aiming to eliminate the need of having output parameters or defining an aggregate type in order to return multiple values from a function. In the K-W C design, tuples can be thought of as merely a syntactic sugar as it is not allowed to define a variable with tuple type. The usage of tuples are restricted to argument passing and assignments, and the translator implementation converts tuple assignments by expanding the tuple assignment expressions to assignments of each component, creating temporary variables to avoid unexpected side effects when necessary. As in the case of a function returning multiple values (thereafter called MVR functions), a struct type is created for the returning tuple and the values are extracted by field access operations.
+
+In an early implementation of tuples in \CFA made by Rodolfo Gabriel Esteves, a different strategy is taken to handle MVR functions. The return values are converted to output parameters passed in by pointers. When the return values of a MVR function are directly used in an assignment expression, the addresses of the left-hand operands can be directly passed in to the function; composition of MVR functions is handled by creating temporaries for the returns.
+
+Suppose we have a function returning two values as follows:
+
+\begin{cfa}
+    [int, int] gives_two();
+
+    int x,y;
+    [x,y] = gives_two();
+\end{cfa}
+
+The K-W C implementation translates the program to
+
+\begin{cfa}
+    struct _tuple2 { int _0; int _1; }
+    struct _tuple2 gives_two();
+    int x,y;
+    struct _tuple2 _tmp = gives_two();
+    x = _tmp._0; y = _tmp._1;
+\end{cfa}
+
+While the Rodolfo implementation translates it to
+
+\begin{cfa}
+    void gives_two(int *, int *);
+    int x,y;
+    gives_two(&x, &y);
+\end{cfa}
+
+and inside the body of the function \text{gives\_two}, the return statement is rewritten to assignments into the passed-in addresses. 
+
+The latter implementation looks much more concise, and in the case of returning values having nontrivial types (e.g. structs), this implementation can also save some unnecessary copying. 
+
+Interestingly, in Robert Schluntz's rework of the tuple type, the implementation got reverted back to struct-based, and it remained in the current version of cfa-cc translator. During the same time of his work, generic types were being added into \CFA independently as another feature, and the tuple type was changed to use the same implementation techniques of generic types. Consequently, it made tuples become first-class values in \CFA. 
+
+However, upon further investigation, making tuple types first-class has very little benefits in \CFA, mainly because that function call semantics with tuples are designed to be unstructured, and that since operator overloading in \CFA are implemented by treating every overloadable operator as functions, tuple types are very rarely used in a structured way. When a tuple-type expression appears in a function call (except assignment expressions, which are handled differently by mass- or multiple-assignment expansions), it is always flattened, and the tuple structure of function parameter is not considered a part of the function signature, for example
+
+\begin{cfa}
+    void f(int, int);
+    void f([int, int]);
+\end{cfa}
+
+are considered to have the same signature (a function taking two ints and returning nothing), and therefore not valid overloads. Furthermore, ordinary polymorphic type parameters are not allowed to have tuple types in order to restrict the expression resolution algorithm to not create too many argument-parameter matching options, such that the type-checking problem remains tractable and does not take too long to compute. Therefore tuple types are never present in any fixed-argument function calls. 
+
+A type-safe variadic argument signature was proposed using \CFA's \texttt{forall} clause and a new tuple parameter type, denoted previously by the \texttt{ttype} keyword and now by the ellipsis syntax similar to \CC's template parameter pack.
+
+The C \texttt{printf} function, for example, can be rewritten using the new variadic argument, in favor of the C untyped \texttt{va\_list} interface as
+
+\begin{cfa}
+    forall (TT...) int printf(char *fmt, TT args);
+\end{cfa}
+
+Note that this is just for illustration purposes, as type assertions are needed to actually achieve type safety, and \CFA's I/O library does not use a format string since argument types are inferred by the type system.
+
+There are two common patterns for using the variadic function in \CFA: one is to forward the arguments to another function
+
+\begin{cfa}
+    forall(T*, TT... | {void ?{}(T &, TT);})
+    T* new (T, TT) { return ((T*)malloc()){TT}; }
+\end{cfa}
+
+and the other is structural recursion which extracts arguments one at a time
+
+\begin{cfa}
+    forall( ostype &, T, Params... | { ostype & ?|?( ostype &, T); ostype & ?|?( ostype &, Params ); } )
+        ostype & ?|?( ostype & os, T arg, Params rest ); 
+\end{cfa}
+
+The above is the actual implementation of variadic print function in \CFA. \texttt{ostype} represents the output stream, similar to \CC's \texttt{ostream} interface. Note that recursion must be used in order to extract type information of the first argument in the list, as opposed to C \texttt{va\_list} variadics which uses a loop to extract each argument, and generally requires some companion data that provides type information, such as the format string in \texttt{printf}.
+
+Variadic polymorphic functions are somehow currently the only place tuple types are used in functions. And just like the case for user-defined generic types, many wrapper functions need to be generated to implement polymorphism with variadics. However, note that the only permitted operations on polymorphic function parameters are given by the assertion (trait) functions, and those eventually need to be supplied flattened tuple arguments, packing the variadic arguments into a rigid struct type and generating all the required wrapper functions become mostly wasted work. Interested readers can refer to pages 77-80 of Robert Schluntz's thesis to see how verbose the translator output needs to be to implement a simple variadic call with 3 arguments, and it will quickly become even worse if the number of arguments is increased: for a call with 5 arguments the translator would have to generate concrete struct types for a 4-tuple and a 3-tuple along with all the polymorphic type data for them! Instead, a much simpler approach of putting all variadic arguments into a data array and providing an offset array to retrieve each individual argument can be utilized. This method is very similar to how the C \texttt{va\_list} object is used, with \CFA type resolver validating and generating the required type information to guarantee type safety.
+
+The print function example
+
+\begin{cfa}
+    forall(T, Params... | { void print(T); void print(Params ); })
+    void print(T arg , Params rest) {
+        print(arg);
+        print(rest);
+    }
+\end{cfa}
+
+using the offset array approach, can be converted to pseudo-\CFA code (ignoring type assertions for T) as
+
+\begin{cfa}
+    void print(T arg, char* _data_rest, size_t* _offset_rest) {
+        print(arg);
+        print(*((typeof rest.0)*) _data_rest, // first element of rest
+            _data_rest + _offset_rest[0],  // remainder of data
+            _offset_rest + 1);  // remainder of offset array
+    }
+\end{cfa}
+
+where the fixed-arg polymorphism for T can be handled by the standard \texttt{void*}-based \CFA polymorphic calling conventions, and the type information can all be deduced at the call site.
+
+Turning tuples into first-class values in \CFA does have a few benefits, namely allowing pointers to tuples and arrays of tuples to exist. However it seems very unlikely that these types can have realistic use cases that are hard to achieve without them. And indeed having the pointer-to-tuple type to exist at all will potentially forbid the simple offset-array implementation of variadic polymorphism (in case that a type assertion requests the pointer type \texttt{Params*} in the above example, forcing the tuple type to be materialized as a struct), and thus incurring a high cost. Perhaps it is of best interest to keep tuples as non-first-class, as Rodolfo originally describes them to "[does] not enforce a particular memory layout, and in particular, [does] not guarantee that the components of a tuple occupy a contiguous region of memory," and therefore to be able to use the simplified implementations for MVR and variadic functions.
+
+One final topic worth discussing is that the strategy of converting return values to output parameters can be utilized to implement copy elision, which is relevant for \CFA since constructors are introduced to the language. However, the first example given in this section
+
+\begin{cfa}
+    int x,y;
+    [x,y] = gives_two();
+\end{cfa}
+
+actually \textit{cannot} have copy elision applied, since the call to \texttt{gives\_two} appears in an \textit{assignment} context rather than an initialization context, as the variables x and y may be already initialized. Unfortunately \CFA currently does not support declaring variables in tuple form:
+
+\begin{cfa}
+    [int x, int y] = gives_two(); // NOT ALLOWED
+\end{cfa}
+
+It is possible to declare a tuple-typed variable and call MVR functions in initialization context
+
+\begin{cfa}
+    [int, int] ret = gives_two(); // OK
+\end{cfa}
+
+but using the values is more awkward as we cannot give them separate names and have to use \texttt{ret.0} or \texttt{ret.1} to extract the values. If copy elision semantics were to be added to \CFA it would be preferable to allow declaring variables in tuple form to have the benefit of eliding copy construction while giving each variable a unique name.
+
+\section{Plan-9 Struct Inheritance}
+
+Plan-9 Inheritance is a non-standard C feature originally introduced by the C dialect used in Bell Labs' Plan-9 research operating system, and is supported by mainstream C compilers such as GCC and Clang. This feature allows an aggregate type (struct or union) to be embedded into another one with implicit access semantics similar to anonymous substructures.
+
+In standard C, it is possible to define a field with an anonymous struct or union type within another. This is often utilized to implement a tagged union:
+
+\begin{cfa}
+
+struct T {
+  unsigned int tag;
+  union {
+    int x;
+    double y;
+    char z;
+  };
+} t;
+\end{cfa}
+
+The union fields can be directly accessed using their names, such as \texttt{T.x}. With Plan-9 extensions enabled, the same can be applied to a struct or union type defined elsewhere. \CFA uses the inline specifier to denote the anonymously embedded field.
+
+In GCC it is possible to simply use\texttt{struct B \{struct A;\}}
+for the Plan-9 feature; since \CFA no longer requires the struct and union keywords in variable declarations, having a keyword to denote Plan-9 inheritance is preferable. 
+
+\begin{cfa}
+  struct A {int x;};
+
+  struct B {
+    inline A;
+    int y;
+  };
+
+  B b;
+  b.x; // accesses the embedded struct A's field
+\end{cfa}
+
+As the \CFA translator simply just reduce the source code to C, usually the non-standard C features do not need any special treatment, and are directly passed down to the C compiler. However, the Plan-9 semantics allow implicit conversions from the outer type to the inner type, which means the type checking algorithm must take that information into account. Therefore, the \CFA translator must implement the Plan-9 features and insert the type conversions into the translated code output. In the current version of \CFA, this is the only kind of implicit type conversion other than the standard C conversions.
+
+Since variable overloading is possible, \CFA's implementation of Plan-9 inheritance allows duplicate field names. When an outer field and an embedded field have the same name and type, the inner field is shadowed and cannot be accessed directly by name. While such definitions are allowed, using duplicate names is not good practice in general and should be avoided if possible.
+
+Plan-9 fields can be nested, and a struct definition can contain multiple Plan-9 embedded fields. In particular, the "diamond pattern" can occur and result in a nested field to be embedded twice.
+
+\begin{cfa}
+  struct A {int x;};
+  struct B {inline A;};
+  struct C {inline A;};
+
+  struct D {
+    inline B;
+    inline C;
+  };
+
+  D d;
+\end{cfa}
+
+In the above example, the expression \texttt{d.x} becomes ambiguous, since it can refer to the indirectly embedded field either from B or from C. It is still possible to disambiguate the expression by first casting the outer struct to one of the directly embedded type, such as \texttt{((B)d).x} 
+
+
+
+

doc/theses/fangren_yu_MMath/content2.tex

@@ -1 @@
-\chapter{Content1}
+\chapter{Resolution Algorithms}
 \label{c:content1}
 
-This chapter ...
-
-\section{Section 1}
-
-\section{Section 2}
+\CFA's type system is fairly complicated. The compiler needs to analyze each expression with many possible forms of overloading. Variables can be overloaded in \CFA, and functions can be overloaded by the argument types as well as the return types. Combined with the polymorphism introduced by forall clauses and generic types, the complexity of expression analysis can go up very quickly. Designing a rule set that behaves mostly as expected, and implementing it as an efficient algorithm for actual use, are both very challenging tasks. As the \CFA translator's performance improves to a level that can compile a mid-sized program in a reasonable amount of time, the development of \CFA's standard library also speeds up and many new features utilizing the expressiveness of \CFA's type system has been implemented, such as generic container types similar to those in \CC's standard template library. During the process of development, many weaknesses and design flaws of \CFA type system have been discovered. Some of those problems arise from the newly introduced language features described in the previous chapter, and fixing those unexpected interactions with the type system is especially difficult. This chapter describes the type resolution rules currently in use and some major problems that have been identified. Not all of those problems have got solutions yet, because fixing them may require redesigning parts of the \CFA language at a larger scale. 
+
+\section{The Expression Cost Model}
+
+\CFA has been using an expression cost model to resolve ambiguity of overloaded expressions from the very beginning. Since most operators can be overloaded in \CFA (excluding a few operators that have special semantics, such as the comma operator, and the short-circuit logical operators \&\& and ||, which require the operands to be evaluated in order), they are treated the same way as other function calls and the same rules for overload resolution must apply to them as well.
+
+In \CFA, candidates of an overloaded expression are ranked by numerical cost elements, that accounts for the type conversions needed from the argument type to the corresponding declared function parameter type, as well as the polymorphic types and restrictions introduces by the forall clause. Currently the expression cost used in \CFA has the following components, ranked from higher to lower by importance:
+
+\begin{enumerate}
+    \item \textbf{Unsafe} cost representing a narrowing conversion of arithmetic types, e.g. \texttt{int} to \texttt{short}, and qualifier-dropping conversions for pointer and reference types;
+    \item \textbf{Polymorphic} cost where the function parameter type is or contains a polymorphic type variable;
+    \item \textbf{Safe} cost representing a widening conversion e.g. \texttt{short} to \texttt{int}, qualifier-adding conversions for pointer and reference types, and value conversion for enumeration constants.
+    \item \textbf{Variable} cost that counts the number of polymorphic variables, if any, introduced by the forall clause in the function declaration;
+    \item \textbf{Specialization} cost that counts the number of restrictions introduced by the type assertions.
+\end{enumerate}
+
+The comparison of cost tuple is by lexicographical order, starting from the highest importance term (unsafe cost) and the lower one has lower cost, with ties going to the second term (polymorphic cost) and so on. At a sub-expression level, the lowest cost candidate for each result type is included as a possible interpretation of the expression; at the top level all possible interpretations of different types are considered and the overall lowest cost is selected as the final interpretation of the expression.
+
+In many languages that support function and operator overloading, such as \CC and Java, a partial ordering system decides which interpretation of the expression gets selected, which means that sometimes the candidates are incomparable (none of those are considered a better match) and only when one candidate is considered better than all others (maximal with respect to the partial order) is the expression unambiguous.
+
+In \CFA trying to use such a system is problematic because of the presence of return type overloading of functions, and overloading of variables. The resolution algorithms used in \CC and Java are greedy, as they select the best match for each sub-expression without considering the higher level ones, and therefore at each step of resolution, the arguments are already given unique interpretations, so the ordering only needs to consider comparing different sets of conversion targets (function parameter types) on the same set of input. However, in \CFA expression resolution considers multiple interpretations of argument sub-expressions with different types, so it is possible that both the selected function and the set of arguments are different, and cannot be compared if we choose to use some kind of partial ordering system. Since this situation can arise quite often in \CFA, even in the simplest form such as an expression \textbf{f(a)} where both the function name \textbf{f} and variable name \textbf{a} are overloaded. We do not want the resolution algorithm to report too many expressions as ambiguous (which would therefore be compilation errors) and restrict the flexibility of \CFA by too much. The previous documentations and papers on \CFA expression resolution never explained why such a cost system is used; this could be a plausible guess of the original motivation of introducing the cost system to \CFA.
+
+On the contrary, using such a cost-based model can sometimes make \CFA expression resolution too permissive; the system will always attempt to select the lowest cost option, and only when there are multiple options tied at the lowest cost it reports the expression as ambiguous. With so many elements in the cost tuple, ties are expected to be uncommon. Other than the case of multiple exact matches which would all have cost of zero, incomparable candidates under a partial ordering of being more specific can often have different expression costs since different kinds of implicit conversions are involved, resulting in seemingly arbitrary overload selections.
+
+Ada is another programming language that has overloading based on return type. Although Ada also allows implicit type conversions of function arguments, it is fairly conservative on resolving ambiguities. There are only two "preference" rules in Ada overload resolution, one for primitive arithmetic operators and one for universal access types (analogous to void* in C); any other cases where an expression have multiple legal interpretations are considered ambiguous. The current overload resolution system for \CFA is on the other end of the spectrum, as it tries to order every legal interpretations of an expression and chooses the best one according to cost, occasionally giving unexpected results.
+
+There are currently at least three different situations where the polymorphic cost element of the cost model does not yield a candidate selection that is clearly justifiable, and one of them is straight up wrong. Here are those three cases:
+
+\begin{enumerate}
+    \item Polymorphic exact match versus non-polymorphic inexact match: consider the following declarations
+
+    \begin{cfa}
+        forall (T) void f (T); // 1
+        void f (long); // 2
+
+        f (42); // currently selects 2
+    \end{cfa}
+
+    Under the current cost model, option 1 incurs a polymorphic cost from matching the argument type \textbf{int} to type variable \textbf{T}, and option 2 incurs a safe cost from integer promotion of type \textbf{int} to \textbf{long}. Since polymorphic cost is ranked above safe conversion cost, option 2 is considered to have lower cost and gets selected. 
+    
+    In contrast, the template deduction and overload resolution rules in \CC selects option 1 instead (converting forall to the equivalent function template declaration). \CC performs template argument deduction and overload candidate ranking in two separate steps: in the first step the type parameters are deduced for each primary function template, and if the corresponding template instantiation succeeds, the resulting function prototype is added to the resolution candidate set. In the second step the implicit conversions (if any) applied to argument types are compared after taking away top-level qualifiers and references, and it prefers an exact match, followed by basic type promotions (roughly corresponds to safe conversion in \CFA), and then other kinds of conversions (roughly corresponds to unsafe conversion in \CFA). Only when the type conversions are the same does it prioritize a non-template candidate. In this example, option 1 produces the prototype void f(int) which gives an exact match and therefore takes priority. The \CC resolution rules effectively makes option 2 a specialization that only applies to type \textbf{long} exactly,\footnote{\CC does have explicit template specializations, however they do not participate directly in overload resolution and can sometimes lead to unintuitive results.} while the current \CFA rules make option 2 apply for all integral types below \textbf{long}. Such a discrepancy could be explained as a design decision that since \CFA polymorphic functions are real entities and are separately compiled, calling them would require passing type information and thus have an actual runtime cost.
+
+    \item Having a lower total polymorphic cost does not always mean a function is more specialized. The following example is taken from Aaron Moss's thesis, which discusses some improvements to the \CFA expression cost model, where he claims the following function prototypes are increasingly more constrained:
+
+    \begin{cfa}
+        forall(T, U) void f(T, U); //1, polymorphic
+        forall(T) void f(T, T); //2, less polymorphic
+        forall(T) void f(T, int); //3, even less polymorphic
+        forall(T) void f(T*, int); //4, least polymorphic
+    \end{cfa}
+
+    This argument is not entirely correct. Although it is true that both the sequence 1,2 and 1,3,4 are increasingly more constrained on the argument  types, the option 2 is not comparable to either of option 3 or 4; they actually describe independent constraints on the two arguments. In natural language, option 3 says that the second argument must have type \textbf{int}, while option 2 says that the two arguments must have the same type. These two constraints can independently be satisfied, therefore neither should be considered a better match when trying to resolve a call to f with argument types (int, int), and reporting such an expression as ambiguous is the most appropriate action. This is a limitation of using a numerical cost value as it cannot these logically complicated cases.
+
+    \item Finally, the introduction of generic types means that it may require more type variables to describe a more specific type and that means simply counting the number of polymorphic type variables is no longer correct in general to order the function candidates as being more constrained. Suppose we have a generic pair type defined and writing a function that takes an arbitrary pair would require using two type variables
+    \begin{cfa}
+        forall (T,U) void f (pair(T,U)); // 1
+    \end{cfa}
+    and compare that with a function that takes any type at all:
+    \begin{cfa}
+        forall (T) void f (T); // 2
+    \end{cfa}
+
+    Passing a pair variable to f gives a cost of 1 poly, 2 variable for the pair overload, and a cost of 1 poly, 1 variable for the unconstrained overload. Clearly we would like the former to be chosen but the cost model cannot handle that correctly. 
+\end{enumerate}
+
+These inconsistencies do not seem to be easily solvable and currently the \CFA codebase has to work around with these known defects. One potential path that could possibly be taken is a mix of the conversion cost and \CC-like partial ordering of specializations. Observe that in the \CFA cost tuple, the first three elements (unsafe, polymorphic and safe conversions) are related to the argument types, while the other elements (polymorphic variable and assertion counts) are properties of the function declarations independent of the arguments. This means it may be reasonable to have an ordering that compares the argument conversion costs first and uses the partial ordering of specializations as a tiebreaker. The algorithm used by \CC template specialization ordering can be applied for \CFA with some slight modifications. 
+
+At the meantime, some other improvements have been made to the expression cost system. Most notably, the expression resolution algorithm now consistently uses the globally minimal cost interpretation, as discussed in a previous technical report. While implementing the change, there are also two detailed issues that need to be addressed for the new rules to fully work.
+
+The first one deals with an idiom commonly used in \CFA that would cause a lot of overloads to have equal costs. These kinds of expressions are so ubiquitous in \CFA code that we do not want them to be deemed ambiguous in the language. Many C library functions have multiple versions for different argument types, for example there are absolute value functions defined for basic arithmetic types with different names, since C does not support any kind of overloading:
+
+\begin{cfa}
+    int abs (int);
+    long labs (long);
+    double fabs (double);
+    float fabsf (float);
+\end{cfa}
+
+It is cumbersome for the programmers to remember all these different function names and select the correct ones, and even worse, if the incorrect version is picked, the program still compiles but with undesired conversions, which can sometimes even change the result, such as using the int version for floating point argument. In \CFA all of these functions are renamed to simply @abs@. This causes multiple overloads to have the same total cost when some conversion is needed. For example @long x = abs(42);@ could be either calling @long abs(long)@ with the argument 42 converted to @long@ or calling @int abs(int)@ and converting the result to @long@. In this example the choice could be arbitrary because both yields identical results. In some other cases, the choice can have an actual impact on the final result. While testing the effects of using the updated cost rule we found this piece of code in \CFA standard library:
+
+\begin{cfa}
+    static inline __readyQ_avg_t __to_readyQ_avg(unsigned long long intsc) {
+        if(unlikely(0 == intsc)) return 0.0; 
+        else return log2(intsc); // implicit conversion happens here
+    } // __readyQ_avg_t is defined to be double
+\end{cfa}
+
+This is a helper function for performance logging that calculate the geometric mean of a counter value, and it does so by summing up the logarithm value of the counter. The function @log2@ is similarly overloaded in \CFA for both integer and floating point types, however in this case, the integer overload returns an integer, so the fractional part of logarithm is truncated. With the previous cost rules the integer version of @log2@ is selected, and when experimenting the updated cost rules this got picked up as an ambiguous expression at first. I reported this issue to the author of library code and got the reply that the expectation was that \CFA would choose the floating point overload, by the return type overloading selection. This mistake went unnoticed since it is only inside a performance logging function and does not serve any critical purposes, and the only effect it has caused is that the performance data becomes inaccurate as the fractional parts got truncated before the sum. Investigating this example leads to the decision that matching the return type higher up in the expression tree is prioritized, in case the total expression cost is equal.
+
+Another change addresses the issue that C arithmetic expressions have unique meanings governed by the arithmetic promotion rules, however in \CFA they are all modelled as function calls for overload resolution purposes. The previous, partially greedy resolution rules will pick the locally optimal match and it matches the C rules naturally. Care needs to be taken to maintain the C semantics when switching to the total expression cost approach. 
+
+This problem is already partially recognized, when Aaron Moss suggested overload resolution by total cost, in the form of handling cast expressions. To quote directly the example:
+
+If a cast argument has an unambiguous interpretation as a conversion argument then it must be interpreted as such, even if the ascription interpretation would have a lower overall cost. This is demonstrated in the following example, adapted from the C standard library:
+
+\begin{cfa}
+    unsigned long long x;
+    (unsigned)(x >> 32);
+\end{cfa}
+
+In C semantics, this example is unambiguously upcasting 32 to @unsigned long long@, performing the shift, then downcasting the result to @unsigned@, at cost (1, 0, 3, 1, 0, 0, 0). If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the @unsigned@ interpretation of @?>>?@ by downcasting x to @unsigned@ and upcasting 32 to @unsigned@, at a total cost of (1, 0, 1, 1, 0, 0, 0). However, this break from C semantics is not backwards compatible, so to maintain C compatibility, the \CFA resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to @unsigned long long@ in the example above, due to the lack of unsafe downcasts), using the cost of the conversion itself only as a tie-breaker.
+
+However, a cast expression is not necessary to have such inconsistency to C semantics. With any implicit argument-parameter type conversion in function calls we can replicate this issue without an explicit cast. For example
+
+\begin{cfa}
+    unsigned long long x;
+    void f (unsigned);
+    f (x >> 32);
+\end{cfa}
+
+This has the same effect as using an explicit cast to coerce the type of expression @x >> 32@ to @unsigned@. This shows that fundamentally the problem is not coming from the cast expressions, but modelling the C built-in operators as overloaded functions. A different rule is enforced in selecting the built-in function candidates to fix this problem. If an expression has any legal interpretations as a C built-in operation, only the lowest cost one is kept, regardless of the result types. 
+
+
+\section{Type Unification}
+
+Type unification is the algorithm that assigns values to each (free) type parameters such that the types of the provided arguments and function parameters match. 
+
+\CFA does not attempt to do any type \textit{inference}: it has no anonymous functions (i.e. lambdas, commonly found in functional programming and also used in \CC and Java), and the variable types must all be explicitly defined (no auto typing). This makes the unification problem more tractable in \CFA as the argument types at each call site are usually all specified. There is a single exception case, which happens when the function return type contains a free type variable that does not occur in any of the argument types, and subsequently passed into the parent expression. A top level expression whose type still contains an unbounded type variable is considered ill-formed as such expression is inherently ambiguous.
+
+The unification algorithm in \CFA is originally presented in Richard Bilson's thesis and it has remained as the basis of the algorithm currently in use. Some additions have been made in order to accommodate for the newly added type features to the language. To summarize, the \CFA type unification has two minor variants: an \textit{exact} mode and an \textit{inexact} mode. The inexact mode is applied at top level argument-parameter matching, and attempts to find an assignment to the type variables such that the argument types can be converted to parameter types with minimal cost as defined in the previous section. The exact mode is required since the type matching algorithm operates recursively and the inner types often have to match exactly, for example there is no common type for the pointer types \textbf{int*} and \textbf{long*} while there is for \textbf{int} and \textbf{long}. With the introduction of generic record types, the parameters must match exactly as well; currently there are no covariance or contravariance supported for the generics.
+
+One simplification was made to the \CFA language that makes modelling the type system easier: polymorphic function pointer types are no longer allowed in declarations. The polymorphic function declarations themselves are still treated as function pointer types internally, however the change means that formal parameter types can no longer be polymorphic. Previously it is possible to write function prototypes such as 
+
+\begin{cfa}
+    void f( forall( T | { T -?( T ); } ) T (*p)( T, T ) );
+\end{cfa}
+
+Notably, the unification algorithm implemented in the \CFA compiler has never managed to trace the assertion parameters on the formal types at all, and the problem of determining if two assertion sets are compatible may very likely be undecidable in general, given the ability of synthesizing more complicated types by the nesting of generics. Eventually, the reason of not allowing such constructs is that they mostly do not provide useful type features for actual programming tasks. A subroutine of a program operates on the arguments provided at the call site together with (if any) local and global variables, and even though the subroutine can be polymorphic, the types will be supported at each call site. On each invocation the types to be operate on can be determined from the arguments provided, and therefore there should not be a need to pass a polymorphic function pointer, which can take any type in principle.
+
+For example, consider a polymorphic function that takes one argument of type \textbf{T} and another pointer to a subroutine
+
+\begin{cfa}
+    forall (T) void f (T x, forall (U) void (*g) (U));
+\end{cfa}
+
+Making \textbf{g} polymorphic in this context would almost certainly be unnecessary, since it can only be called inside the body of \textbf{f} and the types of the argument would have been known anyways, although it can potentially depend on \textbf{T}. Moreover, requesting a function parameter to be able to potentially work on any input type at all would always impose too much constraint on the arguments, as it only needs to make each calls inside the body of \textbf{f} valid.
+
+Rewriting the prototype to
+
+\begin{cfa}
+    forall (T) void f (T x, void (*g) (T));
+\end{cfa}
+
+will be sufficient (or potentially, some compound type synthesized from \textbf{T}), in which case \textbf{g} is no longer a polymorphic type on itself. The "monomorphization" conversion is readily supported in \CFA, either by explicitly assigning a polymorphic function name to a compatible function pointer type, or implicitly done in deducing assertion parameters (which will be discussed in the next section). Such technique can be directly applied to argument passing, which is essentially just assignment to function parameter variables. There might be some edge cases where the supplied subroutine \textbf{g} is called on arguments of different types inside the body of \textbf{f} and so declared as polymorphic, but such use case is rare and the benefit of allowing such constructs seems to be minimal in practice. 
+
+The result of this change is that the unification algorithm no longer needs to distinguish "open" and "closed" type variables, as the latter is not allowed to exist. The only type variables that need to be handled are those introduced by the \textbf{forall} clause from the function prototype. The subtype relationship between function types is now also rendered redundant since none of the function parameter or return types can be polymorphic, and no basic types or non-polymorphic function types are subtypes of any other type. Therefore the goal of (exact) type unification now simply becomes finding a substitution that produces identical types. The assertion set need to be resolved is also always just the declarations on the function prototype, which also simplifies the assertion satisfaction algorithm by a bit, as will be discussed further in the next section.
+
+The type unification results are stored in a type environment data structure, which represents all the type variables currently in scope as equivalent classes, together with their bound types and some other extra information, such as whether the bound type is allowed to be opaque (i.e. a forward declaration without definition in scope), and whether the bounds are allowed to be widened. In the more general approach commonly used in functional languages, the unification variables are given a lower bound and an upper bound to account for covariance and contravariance of types. \CFA currently does not implement any variance with its generic types, and does not allow polymorphic function types, therefore no explicit upper bound is needed and one simple binding value for each equivalence class suffices. However, since type conversions are allowed in \CFA, the type environment needs to keep track on which type variables are allowed conversions. This behavior is notably different from \CC template argument deduction which enforces an exact match everywhere unless the template argument types are explicitly given. For example, a polymorphic maximum function in \CFA can be called with arguments of different arithmetic types and the result follows the usual arithmetic conversion rules, while such expression is not allowed by \CC:
+
+\begin{cfa}
+    forall (T | {int ?<? (T, T); }) T max (T, T);
+
+    max (42, 3.14); // OK, T=double; requires explicit type annotation in C++ such as max<double>(42, 3.14);
+\end{cfa}
+
+The current \CFA documentation does not include a formal set of rules for type unification. In practice, the algorithm implemented in the \CFA translator can be summarized as follows, given a function signature forall$(T_1,..., T_n) f(p_1, ..., p_m)$ and argument types $(a_1, ..., a_m)$, the unification algorithm performs the following steps: \footnote{This assumes argument tuples are already expanded to the individual components.}
+
+\begin{enumerate}
+    \item The type environment is initialized as the union of all type environments of the arguments, plus $(T_1,...,T_n)$ as free variables. The inclusion of argument environments serves the purpose of resolving polymorphic return types that needs to be deduced.
+    \item Initially, all type variables 
+
+\end{enumerate}
+
+
+
+
+
+
+
+\section{Satisfaction of Assertions}
+
+The assertion satisfaction problem greatly increases the complexity of \CFA expression resolution. Past experiments have shown that the majority of time is spent in resolving the assertions for those expressions that takes the longest time to resolve. Even though a few heuristics-based optimizations are introduced to the compiler now, this remains to be the most costly part of compiling a \CFA program. The major difficulty of resolving assertions is that the problem can become recursive, since the expression used to satisfy an outstanding assertion can have its own assertions, and in theory this can go on indefinitely. Detecting infinite recursion cases in general is not algorithmically possible and it is not attempted in the compiler. Instead, a fixed maximum depth of recursive assertions is imposed. This approach is also taken by \CC compilers as template argument deduction is also similarly undecidable in general. 
+
+In previous versions of \CFA this number was set at 4; as the compiler becomes more optimized and capable of handling more complex expressions in a reasonable amount of time, I have increased the limit to 8 and in most occasions it does not lead to trouble. Very rarely there will be a case where the infinite recursion produces an exponentially growing assertion set, causing minutes of time wasted before the limit is reached. Fortunately it is very hard to run into this situation with realistic \CFA code, and the ones that were found all have some clear characteristics, which can be prevented by some clever tricks. In fact, some of the performance optimizations come from analyzing these problematic cases. One example of such will be presented later in this section.
+
+While the assertion satisfaction problem in isolation looks like just another expression to resolve, the recursive nature makes some techniques applied to expression resolution without assertions no longer possible. The most significant impact is that the type unification has a side effect, namely editing the type environment (equivalence classes and bindings), which means that if one expression has multiple associated assertions, they are not independent as the changes to the type environment must be compatible for all the assertions to be resolved. Particularly, if one assertion parameter can be resolved in multiple different ways, all of the results need to be checked to make sure the change to type variable bindings are compatible with other assertions to be resolved. A naive algorithm that simply picks any pending assertion to resolve and continue in a depth-first search could be very inefficient and especially prone of falling into an infinite loop, while in many cases it can be avoided by examining other assertions that can provide insight on the desired type binding: if one assertion parameter can only be matched by a unique option, we can then update the type bindings confidently without the need of backtracking. 
+
+The algorithm currently used in \CFA compiler is designed by Aaron Moss through a simplified prototype experiment that captures most of \CFA type system features and ported back to the actual language. It can be described as a mix of breadth- and depth-first search in a staged approach. 
+
+To resolve a set of assertions, the algorithm first attempts to resolve each assertion item individually. There are three possible outcomes on resolving each assertion:
+
+\begin{enumerate}
+    \item If no matches are found, the algorithm terminates with a failure.
+    \item If exactly one match is found, the type environment is updated immediately, and used in resolving any remaining assertions.
+    \item If multiple matches are found, the assertion candidates with their updated type environments are stored in a list that will be checked for compatibility at the end. 
+\end{enumerate}
+
+When all assertion items are resolved successfully, the algorithm attempts to combine the ambiguously resolved assertions to produce mutually compatible assignments. If any new assertions are introduced by the selected candidates, the algorithm is applied recursively, until there are none pending resolution or the recursion limit is reached which results in a failure.
+
+It has been discovered in practice that the efficiency of such algorithm can sometimes be very sensitive to the order of resolving assertions. Suppose an unbound type variable @T@ appears in two assertions, one can be uniquely resolved and allow the type @T@ to be inferred immediately, and another has many ways to be resolved, each results in @T@ being bound to a different concrete type. If the first assertion is examined first by the algorithm, the deducted type can then be utilized in resolving the second assertion and eliminate many incorrect options without producing the list of candidates pending further checks. In practice, this have a significant impact when an unbound type @T@ is declared to satisfy the basic "object assertions"\footnote{The term is borrowed from object-oriented languages although \CFA is not object-oriented in principle.} of having a default constructor, destructor, and copy assignment operations. Since they are defined for every type currently in scope, there are often hundreds or even thousands of matches to these functions with an unspecified operand type, and in most of the cases the value of @T@ can be deduced by resolving another assertion first, which then allows specific object lifetime functions to be looked up since they are sorted internally by the operand type, and greatly reduces the number of wasted resolution attempts.
+
+Currently this issue also causes the capability of the assertion resolution algorithm to be limited. Assertion matching is implemented to be more restricted than expression resolution in general, in that the parameter types must match exactly, rather than just merely callable. If one function declaration includes an assertion of @void f(T)@ and only a @f(long)@ is currently in scope, trying to resolve the assertion with @T=int@ would not work. Loosening the assertion matching requirement causes many assertion variables to have multiple matches and makes the delayed combination step too costly.
+
+Given all the issues caused by assertion resolution potentially creating new type variable bindings, a natural progression is to put some restrictions on free type variables such that all the type variables will be bound when the expression reaches assertion resolution stage. A type variable introduced by the @forall@ clause of function declaration can appear in parameter types, return types and assertion variables. If it appears in the parameter types, it will be bound when matching the arguments to parameters at the call site. If it only appears in the return type, it can be eventually figured out by the context in principle. The current implementation in \CFA compiler does not do enough return type deduction as it performs eager assertion resolution, and the return type information cannot be known in general before the parent expression is resolved, unless the expression is in an initialization context, in which the type of variable to be initialized is certainly known. By delaying the assertion resolution until the return type becomes known, this problem can be circumvented. The truly problematic case occurs if a type variable does not appear in either of the parameter or return types and only appears in some assertion variables. Such case is very rare and it is not evident that forcing every type variable to appear at least once in parameter or return types limits the expressiveness of \CFA type system to a significant extent. In the next chapter I will discuss about a proposal of including type declarations in traits rather than having all type variables appear in the trait parameter list, which could be helpful for providing equivalent functionality of having an unbound type parameter in assertion variables, and also addressing some of the variable cost issue discussed in section 4.1.
+
+\subsection*{Caching Assertion Resolution Results}
+
+In Aaron Moss's prototype design and experiments, a potential optimization of caching the result of already resolved assertions is discussed. Based on the experiment results, this approach can improve the performance of expression resolution in general, and sometimes allow hard instances of assertion resolution problems to be solved that are otherwise infeasible, for example when the resolution would encounter infinite loops.
+
+The problem that makes this approach tricky to be implemented correctly is that the resolution algorithm has side effects, namely modifying the type bindings in the environment. If we were to cache those results that cause the type bindings to be modified, it would be necessary to store the changes to type bindings too, and in case where multiple candidates can be used to satisfy one assertion parameter, all of them needs to be cached including those that are not eventually selected, since the side effect can produce different results depending on the context. 
+
+In the original design of \CFA that includes unrestricted polymorphic formal parameters that can have assertions on themselves, the problem is even more complicated as new declarations can be introduced in scope during expression resolution. Here is one such example taken from Bilson:
+
+\begin{cfa}
+    void f( forall( T | { T -?( T ); } ) T (*p)( T, T ) );
+    forall( U, V | { U -?( U ); V -?( V ); } ) U g( U, V ) );
+    f( g );
+\end{cfa}
+
+The inner assertion parameter on the \textit{closed} type variable @T@ is used to satisfy the assertions on @U@ and @V@ in this example. 
+
+However, as per the previous discussions on this topic, polymorphic function pointer types have been removed from \CFA, since correctly implementing assertion matching is not possible in general. Without closed parameters (and therefore no have-set for assertions) the set of declarations in scope remains unchanged while resolving any expression. The current \CFA implementation also does not attempt to widen any already bound type parameters to satisfy an assertion. Note that such restriction does mean that certain kinds of expressions cannot be resolved, for example:
+
+\begin{cfa}
+    forall (T | {void f(T);}) void g(T);
+    void f (long);
+    g(42);
+\end{cfa}
+
+The call @g(42)@ is rejected since no attempt is made to widen the parameter type @T@ from @int@ to @long@. Such problem could be mitigated if we allow inexact matches of assertions, but cannot be eliminated completely, if @T@ is matched in a parameterized type, including pointers and references:
+
+\begin{cfa}
+    forall (T | {void f(T*);}) void g(T);
+    void f (long *);
+    g(42);
+\end{cfa}
+
+Here the only way to resolve the call @g(42)@ is to allow assertion resolution to widen the parameter @T@, since even with inexact matching, @int*@ cannot be converted to @long*@. 
+
+
+
+\section{Compiler Implementation Considerations}
+
+

doc/theses/fangren_yu_MMath/performance.tex

@@ -1 @@
-\chapter{Performance}
+\chapter{Future Work}
 
-If there are any performance experiments.
+These are some feature requests related to type system enhancement that come up during the development of \CFA language and library, but have not been implemented yet. A lot of the current implementations have to work around the limits of the language features and sometimes lead to inefficiency. 
+
+\section{Closed trait types}
+
+\CFA as it currently is does not have any closed types, as new functions can be added at any time. It is also possible to locally declare a function\footnote{Local functions are not a standard feature in C but supported by mainstream C compilers such as gcc, and allowed in \CFA too.} or a function pointer to make a type satisfy a certain trait temporarily and be used as such in this limited scope. However, the lack of closed types in such a "duck typing" scheme proposes two problems. For library implementors, it is common to not want the defined set of operations to be overwritten and cause the behavior of polymorphic invocations to change. For the compiler, it means caching and reusing the result of resolution is not reliable as newly introduced declarations can participate in assertion resolution, making a previously invalid expression valid, or the other way around by introducing ambiguity in assertions. Sometimes those interfaces are fairly complicated, for example the I/O library traits \textbf{istream} and \textbf{ostream} each has over 20 operations. Without the ability to store and reuse assertion resolution results, each time the compiler encounters an I/O operation in the source code (mainly the pipe operator \textbf{?|?} used to represent stream operations in \CFA) it has to resolve the same set of assertions again, causing a lot of repetitive work. Previous experiments have shown that the I/O assertions often account for over half of the number of assertions resolved in a \CFA translation unit. Introducing a way to eliminate the need of doing such repetitive assertion resolutions that are very unlikely to change by new overloads can therefore provide significant improvement to the performance of the compiler.
+
+\section{Associated Types}
+
+The analysis presented in section 4.3 shows that if we mandate that all type parameters have to be bound before assertion resolution, the complexity of resolving assertions become much lower as every assertion parameter can be resolved independently. By fully utilizing information from higher up the expression tree for return value overloading, most of the type bindings can be resolved. However there are certain scenarios where we would like to have some intermediate types to be involved in certain operations, that are neither input nor output types.
+
+\CFA standard library provides a few polymorphic container types similar to those found in \CC standard template library. Naturally, we would like to have a harmonized iterator interface for different container types. The feature is still under development and has not been finalized, but for the purpose of this discussion, we will be using a similar approach to the \CC standard iterator contract. The equivalent type signatures can be given in \CFA trait as:
+
+\begin{cfa}
+    forall (Container, Iter, Elem) trait iterable {
+        Iter begin(Container);
+        Iter end(Container);
+        Elem& *?(Iter);
+        Iter ++?(Iter);
+        bool ?==?(Iter,Iter);
+    }
+\end{cfa}
+
+These are the exact operators required in \CC for the for-loop comprehension
+@for (Elem & e: container)@. The problem with this trait declaration is that the iterator type @Iter@ has to be explicitly given in the trait parameter list, but is intended to be deduced from the @begin@ and @end@ operations on the container type; and the same can be said for the element type. The iterable trait is meant to describe a property for the container type but involves two additional types, one for the iterator type and one for the element type. If we were to disallow unbound type parameters in assertions without adding any features to the type system, we will not be able to describe this iterable property in \CFA. 
+
+To solve this problem, I propose adding associate type declarations in addition to the existing (free) @forall@ type parameters. In the body of a trait declaration, new types can be introduced as the return type of an expression involving the type parameters. Following the above example, the iterator contract could be rewritten to
+\begin{cfa}
+    forall (Container) trait iterable {
+        type Iter = begin(Container);
+        type Elem& = *?(Iter);
+        Iter end(Container);
+        Iter ++?(Iter);
+        bool ?==?(Iter,Iter);
+    }
+\end{cfa}
+
+This matches conceptually better that the iterable trait is about one type (the container) rather than about three types. The iterator type and element type can be viewed as properties of the container types, not independent type parameters.
+
+There remains one design decision to be made, that is whether the expressions that define associated types need to be uniquely resolved. If the associated type does not appear in parameter or return types, having such requirement seems to be reasonable, because the expression cost does not consider any conversions that occur in assertion parameter matching, which essentially means having multiple ways to resolve an associated type always results in ambiguity. A more interesting case would be that the associated type also appears in the return type, where both resolving the return type overload based on context and resolving the assertion that defines the associate type can help, and for the whole expression to resolve, they must agree on a common result. Moss gave the following example to illustrate \CFA assertion system's expressiveness that could be viewed as having an associated type as return, and can potentially vary based on the context:
+
+\begin{cfa}
+    forall(Ptr, Elem) trait pointer_like {
+        Elem& *?(Ptr); // Ptr can be dereferenced to Elem
+    };
+    struct list {
+        int value;
+        list* next; // may omit struct on type names
+    };
+    typedef list* list_iterator;
+    int& *?(list_iterator it) {
+        return it->value;
+    }
+\end{cfa}
+
+Note that the type @list*@ satisfies both @pointer_like(list*, int)@ and @pointer_like(list*, list)@ (the latter by the built-in pointer dereference operator) and the expression @*it@ could be either a @struct list@ or an @int@. Requiring associated types to be unique would make the @pointer_like@ trait inapplicable to @list*@ here, which is not desirable. I have not attempted to implement associated types in \CFA compiler, but based on the above discussions, one option could be to make associated type resolution and return type overloading coexist: when the associated type appears in the returns, we deduce it from the context and then verify the trait with ordinary assertion resolution; when it does not appear in the returns, we instead require the type to be uniquely determined by the expression that defines the associated type.
+
+\section{User-defined conversions}

doc/theses/jiada_liang_MMath/CFAenum.tex

@@ -1 +1 @@
 \chapter{\CFA Enumeration}
-
 
 % \CFA supports C enumeration using the same syntax and semantics for backwards compatibility.
@@ -9 +8 @@
 \begin{clang}[identifierstyle=\linespread{0.9}\it]
 $\it enum$-specifier:
-        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit }
-        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { enumerator-list-noinit , }
+        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { cfa-enumerator-list }
+        enum @(type-specifier$\(_{opt}\)$)@ identifier$\(_{opt}\)$ { cfa-enumerator-list , }
         enum @(type-specifier$\(_{opt}\)$)@ identifier
-enumerator-list-noinit:
+cfa-enumerator-list:
+        cfa-enumerator
+        cfa-enumerator, cfa-enumerator-list
+cfa-enumerator:
         enumeration-constant
-        enumerator-list-noinit , enumeration-constant
+        $\it inline$ identifier
+        enumeration-constant = expression
 \end{clang}
-\CFA enumerations, or \CFA enums, have optional type declaration in a bracket next to the enum keyword.
+A \newterm{\CFA enumeration}, or \newterm{\CFA enum}, has an optional type declaration in the bracket next to the @enum@ keyword.
 Without optional type declarations, the syntax defines "opaque enums".
 Otherwise, \CFA enum with type declaration are "typed enums".
@@ -284 +287 @@
 Note, the validity of calls is the same for call-by-reference as for call-by-value, and @const@ restrictions are the same as for other types.
 
-
-
-\section{Enumeration Traits}
-
-\CFA defines the set of traits containing operators and helper functions for @enum@.
-A \CFA enumeration satisfies all of these traits allowing it to interact with runtime features in \CFA.
-Each trait is discussed in detail.
-
-The trait @CfaEnum@:
-\begin{cfa}
-forall( E ) trait CfaEnum {
-        char * label( E e );
-        unsigned int posn( E e );
-};
-\end{cfa}
-
-describes an enumeration as a named constant with position. And @TypeEnum@
-\begin{cfa}
-forall( E, V ) trait TypeEnum {
-        V value( E e );
-};      
-\end{cfa}
-asserts two types @E@ and @T@, with @T@ being the base type for the enumeration @E@. 
-
-The declarative syntax
-\begin{cfa}
-enum(T) E { A = ..., B = ..., C = ... };
-\end{cfa}
-creates an enumerated type E with @label@, @posn@ and @value@ implemented automatically.
-
-\begin{cfa}
-void foo( T t ) { ... }
-void bar(E e) {
-        choose (e) {
-                case A: printf("\%d", posn(e));
-                case B: printf("\%s", label(e));
-                case C: foo(value(e));
-        } 
-}
-\end{cfa}
-
-Implementing general functions across all enumeration types is possible by asserting @CfaEnum( E, T )@, \eg:
-\begin{cfa}
-#include <string.hfa>
-forall( E, T | CfaEnum( E, T ) | {unsigned int toUnsigned(T)} )
-string formatEnum( E e ) {
-        unsigned int v = toUnsigned(value(e));
-        string out = label(e) + '(' + v +')';
-        return out;
-}
-printEunm( Week.Mon );
-printEnum( RGB.Green );
-\end{cfa}
-
-\CFA does not define attribute functions for C style enumeration. But it is possilbe for users to explicitly implement
-enumeration traits for C enum and any other types.
-
-\begin{cfa}
-enum Fruit { Apple, Bear, Cherry };                     $\C{// C enum}$
-char * label(Fruit f) {
-        switch(f) {
-                case Apple: "A"; break;
-                case Bear: "B"; break;
-                case Cherry: "C"; break;
-        }
-}
-unsigned posn(Fruit f) { return f; }
-char* value(Fruit f) { return ""; }             $\C{// value can return any non void type}$
-formatEnum( Apple );                                                    $\C{// Fruit is now a Cfa enum}$
-\end{cfa}
-
-A type that implements trait @CfaEnum@, \ie, a type has no @value@, is called an opaque enum.
-
-% \section{Enumerator Opaque Type}
-
-% \CFA provides a special opaque enumeration type, where the internal representation is chosen by the compiler and only equality operations are available.
-\begin{cfa}
-enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
-\end{cfa}
-
-
-In addition, \CFA implements @Bound@ and @Serial@ for \CFA Enums.
-\begin{cfa}
-forall( E ) trait Bounded {
-        E first();
-        E last();
-};
-\end{cfa}
-The function @first()@ and @last()@ of enumerated type E return the first and the last enumerator declared in E, respectively. \eg:
-\begin{cfa}
-Workday day = first();                                  $\C{// Mon}$
-Planet outermost = last();                              $\C{// NEPTUNE}$
-\end{cfa}
-@first()@ and @last()@ are overloaded with return types only, so in the example, the enumeration type is found on the left-hand side of the assignment.
-Calling either functions without a context results in a type ambiguity, except in the rare case where the type environment has only one enumeration.
-\begin{cfa}
-@first();@                                                              $\C{// ambiguous because both Workday and Planet implement Bounded}$
-sout | @last()@;
-Workday day = first();                                  $\C{// day provides type Workday}$
-void foo( Planet p );
-foo( last() );                                                  $\C{// parameter provides type Planet}$
-\end{cfa}
-
-The trait @Serial@:
-\begin{cfa}
-forall( E | Bounded( E ) ) trait Serial {
-        unsigned fromInstance( E e );
-        E fromInt( unsigned int posn );
-        E succ( E e );
-        E pred( E e );
-};
-\end{cfa}
-is a @Bounded@ trait, where elements can be mapped to an integer sequence.
-A type @T@ matching @Serial@ can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
-%However, the inverse may not be possible, and possible requires a bound check.
-The mapping from a serial type to integer is defined by @fromInstance@, which returns the enumerator's position.
-The inverse operation is @fromInt@, which performs a bound check using @first()@ and @last()@ before casting the integer into an enumerator.
-Specifically, for enumerator @E@ declaring $N$ enumerators, @fromInt( i )@ returns the $i-1_{th}$ enumerator, if $0 \leq i < N$, or raises the exception @enumBound@.
-
-The @succ( E e )@ and @pred( E e )@ imply the enumeration positions are consecutive and ordinal. 
-Specifically, if @e@ is the $i_{th}$ enumerator, @succ( e )@ returns the $i+1_{th}$ enumerator when $e \ne last()$, and @pred( e )@ returns the $i-1_{th}$ enumerator when $e \ne first()$. 
-The exception @enumRange@ is raised if the result of either operation is outside the range of type @E@.
-
-Finally, there is an associated trait defining comparison operators among enumerators. 
-\begin{cfa}
-forall( E, T | CfaEnum( E, T ) ) {
-        // comparison
-        int ?==?( E l, E r );           $\C{// true if l and r are same enumerators}$
-        int ?!=?( E l, E r );           $\C{// true if l and r are different enumerators}$
-        int ?!=?( E l, zero_t );        $\C{// true if l is not the first enumerator}$
-        int ?<?( E l, E r );            $\C{// true if l is an enumerator before r}$
-        int ?<=?( E l, E r );           $\C{// true if l before or the same as r}$
-        int ?>?( E l, E r );            $\C{// true if l is an enumerator after r}$
-        int ?>=?( E l, E r );           $\C{// true if l after or the same as r}$         
-}
-\end{cfa}
-
-
-
-
-
 \section{Enumerator Control Structures}
 
@@ -433 +295 @@
 
 For example, an intuitive use of enumerations is with the \CFA @switch@/@choose@ statement, where @choose@ performs an implicit @break@ rather than a fall-through at the end of a @case@ clause.
-\begin{cquote}
-\begin{cfa}
+(For this discussion, ignore the fact that @case@ requires a compile-time constant.)
+\begin{cfa}[belowskip=0pt]
 enum Count { First, Second, Third, Fourth };
 Count e;
 \end{cfa}
-\begin{tabular}{ll}
-\begin{cfa}
+\begin{cquote}
+\setlength{\tabcolsep}{15pt}
+\noindent
+\begin{tabular}{@{}ll@{}}
+\begin{cfa}[aboveskip=0pt]
 
 choose( e ) {
@@ -449 +314 @@
 \end{cfa}
 &
-\begin{cfa}
+\begin{cfa}[aboveskip=0pt]
 // rewrite
 choose( @value@( e ) ) {
@@ -465 +330 @@
 enum Count { First, Second, Third @= First@, Fourth };
 \end{cfa}
-which make @Third == First@ and @Fourth == Second@, causing a compilation error because of duplicate @case@ clauses.
+making @Third == First@ and @Fourth == Second@, causing a compilation error because of duplicate @case@ clauses.
 To better match with programmer intuition, \CFA toggles between value and position semantics depending on the language context.
 For conditional clauses and switch statements, \CFA uses the robust position implementation.
 \begin{cfa}
-choose( @position@( e ) ) {
-        case @position@( First ): ...;
-        case @position@( Second ): ...;
-        case @position@( Third ): ...;
-        case @position@( Fourth ): ...;
-}
-\end{cfa}
-
-\begin{cfa}
-Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
-p(variable_a); // 0
-p(variable_b); // 1
-p(variable_c); // "Third"
-p(variable_d); // 3
-\end{cfa}
-
-\begin{cfa}
-for (d; Workday) { sout | d; }
-for (p; +~=Planet) { sout | p; }
-for (c: -~=Alphabet ) { sout | c; }
-\end{cfa}
-The @range loop@ for enumeration is a syntax sugar that loops over all enumerators and assigns each enumeration to a variable in every iteration.
-The loop control of the range loop consists of two parts: a variable declaration and a @range expression@, with the type of the variable
-can be inferred from the range expression.
-
-The range expression is an enumeration type, optionally prefixed by @+~=@ or @-~=@. Without a prefix, or prefixed with @+~=@, the control
-loop over all enumerators from the first to the last. With a @-~=@ prefix, the control loops backward.
-
-On a side note, the loop syntax
-\begin{cfa}
-for ( typeof(Workday) d; d <= last(); d = succ(d) );
-\end{cfa}
-does not work. When d == last(), the loop control will still attempt to assign succ(d) to d, which causes an @enumBound@ exception.
-
-\CFA reduces conditionals to its "if case" if the predicate is not equal to ( @!=@ ) zero, and the "else case" otherwise.
-Overloading the @!=@ operator with an enumeration type against the zero defines a conceptual conversion from
-enum to boolean, which can be used as predicates.
-
+if ( @posn@( e ) < posn( Third ) ) ...
+choose( @posn@( e ) ) {
+        case @posn@( First ): ...;
+        case @posn@( Second ): ...;
+        case @posn@( Third ): ...;
+        case @posn@( Fourth ): ...;
+}
+\end{cfa}
+
+\CFA provides a special form of for-control for enumerating through an enumeration, where the range is a type.
+\begin{cfa}
+for ( cx; @Count@ ) { sout | cx | nonl; } sout | nl;
+for ( cx; +~= Count ) { sout | cx | nonl; } sout | nl;
+for ( cx; -~= Count ) { sout | cx | nonl; } sout | nl;
+First Second Third Fourth
+First Second Third Fourth
+Fourth Third Second First
+\end{cfa}
+The enumeration type is syntax sugar for looping over all enumerators and assigning each enumerator to the loop index, whose type is inferred from the range type.
+The prefix @+~=@ or @-~=@ iterate forward or backwards through the inclusive enumeration range, where no prefix defaults to @+~=@.
+
+C has an idiom for @if@ and loop predicates of comparing the predicate result ``not equal to 0''.
+\begin{cfa}
+if ( x + y /* != 0 */ ) ...
+while ( p /* != 0 */ ) ...
+\end{cfa}
+This idiom extends to enumerations because there is a boolean conversion in terms of the enumeration value, if and only if such a conversion is available.
+For example, such a conversion exists for all numerical types (integral and floating-point).
+It is possible to explicitly extend this idiom to any typed enumeration by overloading the @!=@ operator.
+\begin{cfa}
+bool ?!=?( Name n, zero_t ) { return n != Fred; }
+Name n = Mary;
+if ( n ) ... // result is true
+\end{cfa}
+Specialize meanings are also possible.
 \begin{cfa}
 enum(int) ErrorCode { Normal = 0, Slow = 1, Overheat = 1000, OutOfResource = 1001 };
-bool ?!=?(ErrorCode lhs, zero_t) { return value(lhs) >= 1000; }
-ErrorCode code = /.../
-if (code) { scream(); }
-\end{cfa}
-
-Incidentally, \CFA does not define boolean conversion for enumeration. If no 
-@?!=?(ErrorCode, zero_t)@ 
-overloading defined,
-\CFA looks for the boolean conversion in terms of its value and gives a compiler error if no such conversion is available.
-
-\begin{cfa}
-enum(int) Weekday { Mon, Tues, Wed, Thurs, Fri, Sat, Sun, };
-enum() Colour { Red, Green, Blue };
-enum(S) Fruit { Apple, Banana, Cherry }
-Weekday w = ...; Colour c = ...; Fruit f = ...;
-if (w) { ... } // w is true if and only if w != Mon, because value(Mon) == 0 (auto initialized)
-if (c) { ... } // error
-if (s) { ... } // depends on ?!=?(S lhs, zero_t ), and error if no such overloading available
-\end{cfa}
-
-As an alternative, users can define the boolean conversion for CfaEnum:
-
-\begin{cfa}
-forall(E | CfaEnum(E))
-bool ?!=?(E lhs, zero_t) {
-        return posn(lhs) != 0;
-}
-\end{cfa}
-which effectively turns the first enumeration as a logical zero and non-zero for others.
-
-\section{Enumerated Arrays}
-Enumerated arrays use an \CFA array as their index.
-\begin{cfa}
-enum() Colour {
-        Red, Orange, Yellow, Green, Blue, Indigo, Violet
-};
-
-string colourCode[Colour] = { "#e81416", "#ffa500", "#ffa500", "#ffa500", "#487de7", "#4b369d", "#70369d" };
-sout | "Colour Code of Orange is " | colourCode[Orange];
-\end{cfa}
+bool ?!=?( ErrorCode ec, zero_t ) { return ec >= Overheat; }
+ErrorCode code = ...;
+if ( code ) { problem(); }
+\end{cfa}
+
+
+\section{Enumeration Dimension}
+
+\VRef{s:EnumeratorTyping} introduced the harmonizing problem between an enumeration and secondary information.
+When possible, using a typed enumeration for the secondary information is the best approach.
+However, there are times when combining these two types is not possible.
+For example, the secondary information might precede the enumeration and/or its type is needed directly to declare parameters of functions.
+In these cases, having secondary arrays of the enumeration size are necessary.
+
+To support some level of harmonizing in these cases, an array dimension can be defined using an enumerator type, and the enumerators used as subscripts.
+\begin{cfa}
+enum E { A, B, C, N }; // possibly predefined
+float H1[N] = { [A] : 3.4, [B] : 7.1, [C] : 0.01 }; // C
+float H2[@E@] = { [A] : 3.4, [B] : 7.1, [C] : 0.01 }; // CFA
+\end{cfa}
+(Note, C uses the symbol, @'='@ for designator initialization, but \CFA had to change to @':'@ because of problems with tuple syntax.)
+This approach is also necessary for a predefined typed enumeration (unchangeable), when additional secondary-information need to be added.
 
 
@@ -568 +412 @@
 \small
 \begin{cfa}
-struct MR { double mass, radius; };
+struct MR { double mass, radius; };                     $\C{// planet definition}$
 enum( @MR@ ) Planet {                                           $\C{// typed enumeration}$
         //                      mass (kg)   radius (km)

doc/theses/jiada_liang_MMath/background.tex

@@ -6 +6 @@
 The following discussion covers C enumerations.
 
-As discussed in \VRef{s:Aliasing}, it is common for C programmers to ``believe'' there are three equivalent forms of named constants.
+As mentioned in \VRef{s:Aliasing}, it is common for C programmers to ``believe'' there are three equivalent forms of named constants.
 \begin{clang}
 #define Mon 0
@@ -33 +33 @@
 C can simulate the aliasing @const@ declarations \see{\VRef{s:Aliasing}}, with static and dynamic initialization.
 \begin{cquote}
-\begin{tabular}{@{}l@{}l@{}}
-\multicolumn{1}{@{}c@{}}{\textbf{static initialization}} &  \multicolumn{1}{c@{}}{\textbf{dynamic intialization}} \\
+\begin{tabular}{@{}ll@{}}
+\multicolumn{1}{@{}c}{\textbf{static initialization}} &  \multicolumn{1}{c@{}}{\textbf{dynamic intialization}} \\
 \begin{clang}
 static const int one = 0 + 1;
@@ -51 +51 @@
         int va[r];
 }
-
-
 \end{clang}
 \end{tabular}
 \end{cquote}
-However, statically initialized identifiers can not appear in constant-expression contexts, \eg @case@.
+However, statically initialized identifiers cannot appear in constant-expression contexts, \eg @case@.
 Dynamically initialized identifiers may appear in initialization and array dimensions in @g++@, which allows variable-sized arrays on the stack.
 Again, this form of aliasing is not an enumeration.
-
 
 \section{C Enumeration}
@@ -129 +126 @@
 
 
-\subsection{Representation}
-
-C standard specifies enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
-In practice, C uses @int@ as the underlying type for enumeration variables, because of the restriction to integral constants, which have type @int@ (unless qualified with a size suffix).
+\subsection{Implementation}
+\label{s:CenumImplementation}
+
+In theory, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
+In practice, C defines @int@~\cite[\S~6.4.4.3]{C11} as the underlying type for enumeration variables, restricting initialization to integral constants, which have type @int@ (unless qualified with a size suffix).
+However, type @int@ is defined as:
+\begin{quote}
+A ``plain'' @int@ object has the natural size suggested by the architecture of the execution environment (large enough to contain any value in the range @INT_MIN@ to @INT_MAX@ as defined in the header @<limits.h>@).~\cite[\S~6.2.5(5)]{C11}
+\end{quote}
+Howeveer, @int@ means a 4 bytes on both 32/64-bit architectures, which does not seem like the ``natural'' size for a 64-bit architecture.
+Whereas, @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
+In reality, both @gcc@ and @clang@ partially ignore this specification and type the integral size of an enumerator based its initialization.
+\begin{cfa}
+enum E { IMin = INT_MIN, IMax = INT_MAX,
+                         ILMin = LONG_MIN, ILMax = LONG_MAX,
+                         ILLMin = LLONG_MIN, ILLMax = LLONG_MAX };
+int main() {
+        printf( "%zd %d %d\n%zd %ld %ld\n%zd %ld %ld\n",
+                         sizeof(IMin), IMin, IMax,
+                         sizeof(ILMin), ILMin, ILMax,
+                         sizeof(ILLMin), ILLMin, ILLMax );
+}
+4 -2147483648 2147483647
+8 -9223372036854775808 9223372036854775807
+8 -9223372036854775808 9223372036854775807
+\end{cfa}
+Hence, initialization in the range @INT_MIN@..@INT_MAX@ is 4 bytes, and outside this range is 8 bytes.
 
 \subsection{Usage}
@@ -150 +170 @@
 enum Week { Mon, Tue, Wed, Thu, Fri, Sat, Sun };
 switch ( week ) {
-        case Mon: case Tue: case Wed: case Thu: case Fri:
+        case Mon ... Fri:                               $\C{// gcc case range}$
                 printf( "weekday\n" );
         case Sat: case Sun:
                 printf( "weekend\n" );
 }
-for ( enum Week day = Mon; day <= Sun; day += 1 ) { // step of 1
+for ( enum Week day = Mon; day <= Sun; day += 1 ) { $\C{// step of 1}$
         printf( "day %d\n", day ); // 0-6
 }
@@ -177 +197 @@
 }
 \end{cfa}
-However, for typed enumerations, \see{\VRef{f:EumeratorTyping}}, this idiom fails.
-
-This idiom leads to another C idiom using an enumeration with matching companion information.
+However, for non-integral typed enumerations, \see{\VRef{f:EumeratorTyping}}, this idiom fails.
+
+This idiom is used in another C idiom for matching companion information.
 For example, an enumeration is linked with a companion array of printable strings.
 \begin{cfa}
@@ -196 +216 @@
 
 \bigskip
-While C provides a true enumeration, it is restricted, has unsafe semantics, and does provide useful enumeration features in other programming languages.
+While C provides a true enumeration, it is restricted, has unsafe semantics, and does not provide useful enumeration features in other programming languages.
 
 \section{\CFA Polymorphism}
@@ -238 +258 @@
 \subsection{Constructor and Destructor}
 In \CFA, all objects are initialized by @constructors@ during its allocation, including basic types, 
-which are initialized by constructors default-generated by a compiler.
+which are initialized by auto-generated basic type constructors.
 
 Constructors are overloadable functions with name @?{}@, return @void@, and have at least one parameter, which is a reference

doc/theses/jiada_liang_MMath/implementation.tex

@@ -1 +1 @@
 \chapter{Enumeration Implementation}
+
+\section{Enumeration Traits}
+
+\CFA defines a set of traits containing operators and helper functions for @enum@.
+A \CFA enumeration satisfies all of these traits allowing it to interact with runtime features in \CFA.
+Each trait is discussed in detail.
+
+The trait @CfaEnum@:
+\begin{cfa}
+forall( E ) trait CfaEnum {
+        const char * @label@( E e );
+        unsigned int @posn@( E e );
+};
+\end{cfa}
+asserts an enumeration type @E@ has named enumerator constants (@label@) with positions (@posn@).
+
+The trait @TypedEnum@ extends @CfaEnum@:
+\begin{cfa}
+forall( E, V | CfaEnum( E ) ) trait TypedEnum {
+        V @value@( E e );
+};
+\end{cfa}
+asserting an enumeration type @E@ can have homogeneous enumerator values of type @V@.
+
+The declarative syntax
+\begin{cfa}
+enum(T) E { A = ..., B = ..., C = ... };
+\end{cfa}
+creates an enumerated type E with @label@, @posn@ and @value@ implemented automatically.
+\begin{cfa}
+void foo( T t ) { ... }
+void bar(E e) {
+        choose ( e ) {
+                case A: printf( "\%d", posn( e) );
+                case B: printf( "\%s", label( e ) );
+                case C: foo( value( e ) );
+        } 
+}
+\end{cfa}
+
+Implementing general functions across all enumeration types is possible by asserting @CfaEnum( E, T )@, \eg:
+\begin{cfa}
+#include <string.hfa>
+forall( E, T | CfaEnum( E, T ) | {unsigned int toUnsigned(T)} )
+string formatEnum( E e ) {
+        unsigned int v = toUnsigned( value( e ) );
+        string out = label(e) + '(' + v +')';
+        return out;
+}
+formatEnum( Week.Mon );
+formatEnum( RGB.Green );
+\end{cfa}
+
+\CFA does not define attribute functions for C-style enumeration.
+But it is possible for users to explicitly implement enumeration traits for C enum and any other types.
+\begin{cfa}
+enum Fruit { Apple, Pear, Cherry };                     $\C{// C enum}$
+const char * label( Fruit f ) {
+        choose ( f ) {
+                case Apple: return "Apple";
+                case Bear: return "Pear";
+                case Cherry: return "Cherry";
+        }
+}
+unsigned posn( Fruit f ) { return f; }
+const char * value( Fruit f ) { return ""; } $\C{// value can return any non void type}$
+formatEnum( Apple );                                            $\C{// Fruit is now a \CFA enum}$
+\end{cfa}
+
+A type that implements trait @CfaEnum@, \ie, a type has no @value@, is called an opaque enum.
+
+% \section{Enumerator Opaque Type}
+
+% \CFA provides a special opaque enumeration type, where the internal representation is chosen by the compiler and only equality operations are available.
+\begin{cfa}
+enum@()@ Planets { MERCURY, VENUS, EARTH, MARS, JUPITER, SATURN, URANUS, NEPTUNE };
+\end{cfa}
+
+
+In addition, \CFA implements @Bound@ and @Serial@ for \CFA enumerations.
+\begin{cfa}
+forall( E ) trait Bounded {
+        E first();
+        E last();
+};
+\end{cfa}
+The function @first()@ and @last()@ of enumerated type E return the first and the last enumerator declared in E, respectively. \eg:
+\begin{cfa}
+Workday day = first();                                  $\C{// Mon}$
+Planet outermost = last();                              $\C{// NEPTUNE}$
+\end{cfa}
+@first()@ and @last()@ are overloaded with return types only, so in the example, the enumeration type is found on the left-hand side of the assignment.
+Calling either functions without a context results in a type ambiguity, except in the rare case where the type environment has only one enumeration.
+\begin{cfa}
+@first();@                                                              $\C{// ambiguous because both Workday and Planet implement Bounded}$
+sout | @last()@;
+Workday day = first();                                  $\C{// day provides type Workday}$
+void foo( Planet p );
+foo( last() );                                                  $\C{// argument provides type Planet}$
+\end{cfa}
+
+The trait @Serial@:
+\begin{cfa}
+forall( E | Bounded( E ) ) trait Serial {
+        unsigned fromInstance( E e );
+        E fromInt( unsigned int posn );
+        E succ( E e );
+        E pred( E e );
+};
+\end{cfa}
+is a @Bounded@ trait, where elements can be mapped to an integer sequence.
+A type @T@ matching @Serial@ can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
+%However, the inverse may not be possible, and possible requires a bound check.
+The mapping from a serial type to integer is defined by @fromInstance@, which returns the enumerator's position.
+The inverse operation is @fromInt@, which performs a bound check using @first()@ and @last()@ before casting the integer into an enumerator.
+Specifically, for enumerator @E@ declaring $N$ enumerators, @fromInt( i )@ returns the $i-1_{th}$ enumerator, if $0 \leq i < N$, or raises the exception @enumBound@.
+
+The @succ( E e )@ and @pred( E e )@ imply the enumeration positions are consecutive and ordinal. 
+Specifically, if @e@ is the $i_{th}$ enumerator, @succ( e )@ returns the $i+1_{th}$ enumerator when $e \ne last()$, and @pred( e )@ returns the $i-1_{th}$ enumerator when $e \ne first()$. 
+The exception @enumRange@ is raised if the result of either operation is outside the range of type @E@.
+
+Finally, there is an associated trait defining comparison operators among enumerators. 
+\begin{cfa}
+forall( E, T | CfaEnum( E, T ) ) {
+        // comparison
+        int ?==?( E l, E r );           $\C{// true if l and r are same enumerators}$
+        int ?!=?( E l, E r );           $\C{// true if l and r are different enumerators}$
+        int ?!=?( E l, zero_t );        $\C{// true if l is not the first enumerator}$
+        int ?<?( E l, E r );            $\C{// true if l is an enumerator before r}$
+        int ?<=?( E l, E r );           $\C{// true if l before or the same as r}$
+        int ?>?( E l, E r );            $\C{// true if l is an enumerator after r}$
+        int ?>=?( E l, E r );           $\C{// true if l after or the same as r}$         
+}
+\end{cfa}
+
+As an alternative, users can define the boolean conversion for CfaEnum:
+
+\begin{cfa}
+forall(E | CfaEnum(E))
+bool ?!=?(E lhs, zero_t) {
+        return posn(lhs) != 0;
+}
+\end{cfa}
+which effectively turns the first enumeration as a logical zero and non-zero for others.
+
+\begin{cfa}
+Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
+p(variable_a); // 0
+p(variable_b); // 1
+p(variable_c); // "Third"
+p(variable_d); // 3
+\end{cfa}
+
+
+\section{Enumeration Variable}
+
+Although \CFA enumeration captures three different attributes, an enumeration instance does not store all this information.
+The @sizeof@ a \CFA enumeration instance is always 4 bytes, the same size as a C enumeration instance (@sizeof( int )@).
+It comes from the fact that:
+\begin{enumerate}
+\item
+a \CFA enumeration is always statically typed;
+\item
+it is always resolved as one of its attributes regarding real usage.
+\end{enumerate}
+When creating an enumeration instance @colour@ and assigning it with the enumerator @Color.Green@, the compiler allocates an integer variable and stores the position 1.
+The invocations of $positions()$, $value()$, and $label()$ turn into calls to special functions defined in the prelude:
+\begin{cfa}
+position( green );
+>>> position( Colour, 1 ) -> int
+value( green );
+>>> value( Colour, 1 ) -> T
+label( green );
+>>> label( Colour, 1) -> char *
+\end{cfa}
+@T@ represents the type declared in the \CFA enumeration defined and @char *@ in the example.
+These generated functions are $Companion Functions$, they take an $companion$ object and the position as parameters.
+
 
 \section{Enumeration Data}

doc/theses/jiada_liang_MMath/intro.tex

@@ -4 +4 @@
 Constants can be overloaded among types, \eg @0@ is a null pointer for all pointer types, and the value zero for integer and floating-point types.
 (In \CFA, the constants @0@ and @1@ can be overloaded for any type.)
-A constant's symbolic name is dictated by language syntax related to types.
+A constant's symbolic name is dictated by language syntax related to types, \eg @5.@ (double), @5.0f@ (float), @5l@ (long double).
 In general, the representation of a constant's value is \newterm{opaque}, so the internal representation can be chosen arbitrarily.
 In theory, there are an infinite set of constant names per type representing an infinite set of values.
@@ -13 +13 @@
 
 Many programming languages capture this important software-engineering capability through a mechanism called \newterm{constant} or \newterm{literal} naming, where a new constant is aliased to an existing constant.
-Its purpose is for readability, replacing a constant name that directly represents a value with a name that is more symbolic and meaningful in the context of the program.
+Its purpose is for readability: replacing a constant name that directly represents a value with a name that is more symbolic and meaningful in the context of the program.
 Thereafter, changing the aliasing of the new constant to another constant automatically distributes the rebinding, preventing errors.
 % and only equality operations are available, \eg @O_RDONLY@, @O_WRONLY@, @O_CREAT@, @O_TRUNC@, @O_APPEND@.
@@ -67 +67 @@
 \label{s:Terminology}
 
-The term \newterm{enumeration} defines a type with a set of new constants, and the term \newterm{enumerator} represents an arbitrary alias name \see{\VRef{s:CEnumeration} for the name derivation}.
-As well, an enumerated type can have three fundamental properties, \newterm{label}, \newterm{order}, and \newterm{value}.
+The term \newterm{enumeration} defines a type with a set of new constants, and the term \newterm{enumerator} represents an arbitrary alias name \see{\VRef{s:CEnumeration} for the name derivations}.
+An enumerated type can have three fundamental properties, \newterm{label} (name), \newterm{order} (position), and \newterm{value} (payload).
 \begin{cquote}
 \sf\setlength{\tabcolsep}{3pt}
@@ -111 +111 @@
 \end{cfa}
 The alias name is logically replaced in the program text by its matching constant.
-It is possible to compare aliases, if the constants allow it, \eg @Size < Pi@;
-whereas \eg @Pi < Name@ might be disallowed depending on the language.
+It is possible to compare aliases, if the constants allow it, \eg @Size < Pi@, whereas @Pi < Name@ might be disallowed depending on the language.
 
 Aliasing is not macro substitution, \eg @#define Size 20@, where a name is replaced by its value \emph{before} compilation, so the name is invisible to the programming language.
@@ -133 +132 @@
 Any reordering of the enumerators requires manual renumbering.
 \begin{cfa}
-const Sun = 1, Mon = 2, Tue = 3, Wed = 4, Thu = 5, Fri = 6, Sat = 7;
+const @Sun = 1@, Mon = 2, Tue = 3, Wed = 4, Thu = 5, Fri = 6, Sat = 7;
 \end{cfa}
 For these reasons, aliasing is sometimes called an enumeration.