source: doc/theses/jiada_liang_MMath/trait.tex @ d6c5faa

Last change on this file since d6c5faa was 96de72b, checked in by JiadaL <j82liang@…>, 32 hours ago
  1. Update contribution; 2. update loop subsection; 3. rangeLoops.cfa are the code example used in loop section
  • Property mode set to 100644
File size: 19.8 KB
Line 
1\chapter{Enumeration Traits}
2\label{c:trait}
3
4% Despite parametric polymorphism being a pivotal feature of \CFA, for a long time, there was not
5% a technique to write functions being polymorphic over enumerated types.
6\CC introduced @std::is_enum@ trait on \CC{11} and @concepts@ on \CC{20}; with the combination, users can
7write function polymorphic over enumerated type in \CC:
8\begin{cfa}
9#include <type_traits>
10
11template<typename T>
12@concept Enumerable = std::is_enum<T>::value;@
13
14template<@Enumerable@ T>
15void f(T) {}
16\end{cfa}
17The @std::is_enum@ and other \CC @traits@ are a compile-time interfaces to query type information.
18While named the same as @trait@, it is orthogonal to \CFA trait, as the latter being defined as
19a collection of assertion to be satisfied by a polymorphic type.
20
21\CFA provides @CfaEnum@ and @TypedEnum@ traits to supports polymorphic functions for \CFA enumeration:
22\begin{cfa}
23forall(T | @CfaEnum(T)@)
24void f(T) {}
25\end{cfa}
26
27\section{CfaEnum and TypedEnum}
28\CFA defines attribute functions @label()@ and @posn()@ for all \CFA enumerations,
29and therefore \CFA enumerations fulfills the type assertions with the combination.
30With the observation, we define trait @CfaEnum@:
31\begin{cfa}
32forall( E ) trait CfaEnum {
33        const char * @label@( E e );
34        unsigned int @posn@( E e );
35};
36\end{cfa}
37
38% The trait @TypedEnum@ extends @CfaEnum@ with an additional value() assertion:
39Typed enumerations are \CFA enumeration with an additional @value@ attribute. Extending
40CfaEnum traits, TypedEnum is a subset of CFAEnum that implements attribute function @value()@,
41which includes all typed enumerations.
42\begin{cfa}
43forall( E, V | CfaEnum( E ) ) trait TypedEnum {
44        V @value@( E e );
45};
46\end{cfa}
47Type parameter V of TypedEnum trait binds to return type of @value()@, which is also the base
48type for typed enumerations. CfaEnum and TypedEnum triats constitues a CfaEnum function interfaces, as well a way to define functions
49over all CfaEnum enumerations.
50\begin{cfa}
51// for all type E that implements value() to return type T, where T is a type that convertible to string
52forall(  E, T | TypedEnum( E, T ) | { ?{}(string &, T ); } )
53string format_enum( E e ) { return label(E) + "(" + string(value(e)) + ")"; }
54
55// int is convertible to string; implemented in the standard library
56enum(int) RGB { Red = 0xFF0000, Green = 0x00FF00, Blue = 0x0000FF };
57
58struct color_code { int R; int G; int B };
59// Implement color_code to string conversion
60?{}(string & this, struct color_code p ) {
61        this = string(p.R) + ',' + string(p.G) + ',' + string(p.B);
62}
63enum(color_code) Rainbow {
64        Red = {255, 0, 0}, Orange = {255, 127, 0}, Yellow = {255, 255, 0}, Green = {0, 255, 0},
65        Blue = {0, 0, 255}, Indigo = {75, 0, 130}, Purple = {148, 0, 211}
66};
67
68format_enum(RGB.Green); // "Green(65280)"
69format_enum(Rainbow.Green); // "Green(0,255,0)"
70\end{cfa}
71
72
73% Not only CFA enumerations can be used with CfaEnum trait, other types that satisfy
74% CfaEnum assertions are all valid.
75Types does not need be defined as \CFA enumerations to work with CfaEnum traits. CfaEnum applies to any type
76with @label()@ and @value()@ being properly defined.
77Here is an example on how to extend a C enumeration to comply CfaEnum traits:
78\begin{cfa}
79enum Fruit { Apple, Banana, Cherry };                   $\C{// C enum}$
80const char * label( Fruit f ) {
81        choose( f ) {
82                case Apple: return "Apple";
83                case Banana: return "Banana";
84                case Cherry: return "Cherry";
85        }
86}
87unsigned posn( Fruit f ) { return f; } 
88char value( Fruit f ) { 
89        choose(f)  {
90                case Apple: return 'a';
91                case Banana: return 'b';
92                case Cherry: return 'c';
93        }
94}
95
96format_enum(Cherry); // "Cherry(c)"
97\end{cfa}
98
99\section{Discussion: Static Type Information}
100@CfaEnum@ and @TypedEnum@ are approximations to \CFA Enumerations and Typed Enumerations: they are not
101assertions on a type being an enumerated type,
102but rather types being shared an interfaces with \CFA enumerations.
103\CC's @type_traits@ is fundamentally different than \CFA's traits: \CC's @type_traits@ are descriptions
104of compile time type information
105\footnote{Concepts can check if a \CC class implement a certain method,
106but it is to probe a static type information of a class having a such member.}
107, while \CFA's trait describe how a type can be used,
108which is a closer paradigm to a trait system in languages such as Scala and Rust.
109However, Scala and Rust's traits are nominative:
110a type explicitly declare a named traits to be of its type; while in \CFA,
111type implements all functions declares in a trait to implicitly be of the trait type.
112
113If to support static type information, \CFA needs new piece of syntax to distinguish static type
114query from function calls, for example:
115\begin{cfa}
116forall(T | { T::is_enum; });
117\end{cfa}
118When to call a polymorphic function @foo(T)@ with assertions set @S@ and function call argument @a@, \CFA 
119determines if there is an overloaded name @a@ that has non-zero conversion cost to all assertions in @S@.
120As a consequence, @is_enum@ can be a \CFA directive that immediately trim down the search space of @a@ to
121be some enumerated types. In fact, because \CFA stores symbols maps to enumeration in a standalone data structure.
122Limiting search space to enumeration improve on \CFA resolution speed.
123
124While assertion on static type information seems improvement on expressivity, it is a challenge to
125extend its capability without a fully functional pre-processsor that evaluate constant expression as \CC 
126compilers does. The described @is_enum@ manipulate compiler behaviour, which cannot be easily extended to
127other usage cases. Therefore, \CFA currently does not support @is_enum@ and utalizes traits as a workaround.
128
129
130\section{Bounded and Serial}
131A bounded type defines a lower bound and a upper bound.
132\begin{cfa}
133forall( E ) trait Bounded {
134        E lowerBound();
135        E lowerBound();
136};
137
138\end{cfa}
139Both Bounded functions are implement for \CFA enumerations, with @lowerBound()@ returning the first enumerator and @upperBound()@ returning
140the last enumerator.
141\begin{cfa}
142Workday day = lowerBound();                                     $\C{// Mon}$
143Planet outermost = upperBound();                                $\C{// NEPTUNE}$
144\end{cfa}
145
146The lowerBound() and upperBound() are functions overloaded on return type only, means their type resolution solely depend on the outer context,
147including expected type as a function argument, or the left hand size of an assignment expression.
148Calling either function without a context results in a type ambiguity, except in the rare case where the type environment has only one
149type overloads the functions, including \CFA enumerations, which has Bounded functions automatic defined.
150\begin{cfa}
151@lowerBound();@                 $\C{// ambiguous as both Workday and Planet implement Bounded}$
152sout | @lowerBound()@;
153Workday day = first();          $\C{// day provides type Workday}$
154void foo( Planet p );
155foo( last() );                      $\C{// argument provides type Planet}$
156\end{cfa}
157
158@Serial@ is a subset of @Bounded@, with functions maps elements against integers, as well implements a sequential order between members.
159\begin{cfa}
160forall( E | Bounded( E ) ) trait Serial {
161        unsigned fromInstance( E e );
162        E fromInt( unsigned int i );
163        E succ( E e );
164        E pred( E e );
165        unsigned Countof( E e );
166};
167\end{cfa}
168
169% A Serail type can project to an unsigned @int@ type, \ie an instance of type T has a corresponding integer value.
170Function @fromInstance()@ projects a @Bounded@ member to a number and @fromInt@ is the inverser. Function @succ()@ take an element, returns the "next"
171member in sequential order and @pred()@ returns the "last" member.
172
173A Serial type E may not be having a one-to-one mapping to integer because of bound. An integer that cannot be mapping to a member of E is called the member \newterm{out of bound}.
174Calling @succ()@ on @upperBound@ or @pred()@ on @lowerBound()@ results in out of bound.
175
176\CFA implements Serial interface for CFA enumerations with \newterm{bound check} on @fromInt()@, @succ()@ and @pred()@, and abort the program if the function call results in out of bound.
177Unlike a cast, conversion between \CFA enumeration and integer with @Serial@ interface is type safe.
178Specifically for @fromInt@, \CFA abort if input i smaller than @fromInstance(lowerBound())@ or greater than @fromInstance(upperBound())@
179
180Function @Countof@ takes an object as a parameter and returns the number of elements in the Serial type, which is @fromInstance( upper ) - fromInstance( lower ) + 1@.
181@Countof@ does not use its arugment as procedural input; it needs
182an argument to anchor its polymorphic type T.
183
184\CFA has an expression @countof@ (lower case) that returns the number of enumerators defined for enumerations.
185\begin{cfa}
186enum RGB {Red, Green, Blue};
187countof( RGB );
188countof( Red );
189\end{cfa}
190Both expressions from the previous example are converted to constant expression @3@ with no function call at runtime.
191@countof@ also works for any type T that defines @Countof@ and @lowerBound@, for which it turns into
192a function call @Countof( T )@. The resolution step on expression @countof(e)@ works as the following with priority ordered:
193\begin{enumerate}
194\item Looks for an enumeration named e, such as @enum e {... }@.
195If such an enumeration e exists, \CFA replace @countof(e)@  with constant expression with number of enumerator of e.
196\item Looks for a non-enumeration type named e that defines @Countof@ and @lowerBound@, including e being a polymorphic type, such as @forall(e)@.
197If type e exists, \CFA replaces it with @Countof(lowerBound())@, where lowerBound() is bounded to type e. 
198\item Looks for an enumerator e that defined in enumeration E. If such an enumeration e exists, \CFA replace @countof(e)@ with constant expression with number of enumerator of E.
199\item Looks for a name e in the context with expression type E. If such name e exists, \CFA replace @countof(e)@ with function call @Countof(e)@.
200\item If 1-4 fail, \CFA reports a type error on expression @countof(e)@.
201\end{enumerate}
202
203\section{Iterating Over An Enumeration}
204An fundamental aspect of an enumerated type is to be able to enumerate over its enumerators. \CFA supports \newterm{for} loops,
205\newterm{while} loop, and \newterm{range} loop. This section covers @for@ loops and @range@ loops for
206enumeration, but the concept transition to @while@ loop.
207
208\subsection{For Loop}
209A for loop is constitued by a loop control and a loop body.
210A loop control is often a 3-tuple, separated by semicolons: initializers, condition, and an expression. It is a common practice to declare
211a variable, often in initializers, that be used in the condition and updated in the expression or loop body. Such variable is called \newterm{index}.
212
213% With implemented @Bounded@ and @Serial@ interface for \CFA enumeration, a @for@ loop that iterates over \CFA enumeration can be implemented as the following:
214A @for@ loop iterates an enumeration can be written with functions from @Bounded@ and @Serial@ interfaces:
215\begin{cfa}
216enum() Chars { A, B, C, D };
217for( unsigned i = 0; i < countof(E); i++ ) { sout | label(e); }         $\C{// (1) A B C D}$
218for( Chars e = lowerBound(); ; e = succ(e) ) { $\C{// (2)}$
219        sout |label((Chars)fromInt(i)) |' ';
220        if (e == upperBound()) break;
221}
222\end{cfa}
223
224A caveat in writing loop using finite number as index is that the number can unintentionally be out the range:
225\begin{cfa}
226for( unsigned i = countof(Chars) - 1; i >= 0; i-- ) {}                          $\C{// 3}$
227for( Chars e = lowerBound(); e <= upperBound(); e = succ(e) ) {}        $\C{// 4}$
228for( Chars e = upperBound(); e >= lowerBound(); e = pred(e) ) {}        $\C{// 5}$
229\end{cfa}
230Loop (3) is a value underflow: when @i@ reaches to @0@, decrement statement will still execute and cause
231the @unsigned int@ value @i@ wraps to @UINT_MAX@, which fails to loop test and the loop cannot terminate.
232
233In loop (4) and (5), when @e@ is at the @Bound@ (@upperBound@/@lowerBound@) and @succ@/@pred@ will result in @out of bounded@, \CFA 
234aborts its execution. Therefore, it is necessary to implement the condtional break within the loop body.
235
236
237\subsection{Range Loop}
238Instead of specifying condition, \CFA supports @range loops@, for which a user specifies a range of values.
239\begin{cfa}[label=lst:range_functions_2]
240for ( Chars e; A ~= D ) { sout | label(e); }            $\C{// (6)}$
241for ( e; A ~= D ) { sout | label(e); }                          $\C{// (7)}$
242for ( Chars e; A -~= D ) { sout | label(e); }           $\C{// (8) D C B A}$
243for ( e; A -~=D ~ 2 ) { sout | label(e); }              $\C{// (9) D B }$
244\end{cfa}
245Every range loop above has an index declaration, and a @range@ bounded by \newterm{left bound} @A@ and \newterm{right bound} @D@.
246An index declaration can have an optional type declaration, without which \CFA 
247implicitly declares index variable to be the type of the bounds (@typeof(A)@).
248If a range is joined by @~=@ (range up equal) operator, the index variable will be initialized by
249the @left bound@, and change incrementally until its position exceeds @right bound@.
250On the other hand, if a range is defined with @-~=@ (range down equal) operation, the index variable will
251have the value of the @right bound@. It change decrementally until its position is less than the @left bound@.
252A range can be suffixed by an positive integal \newterm{step}, joined by @~@. The loop @(9)@ declares a step size of 2 so that
253e updates @pred(pred(e))@ in every iteration.
254
255\CFA manipulates the position of the index variable and breaks the loop if an index update can result in @out of range@.
256
257\CFA provides a shorthand for range loop over a \CFA enumeration or a @Serial@:
258\begin{cfa}[label=lst:range_functions_2]
259for ( e; Chars ) { sout | label(e); }           $\C{// (10) A B C D}$
260for ( e; E ) {                                                          $\C{// forall(E | CfaEnum(E) | Serial(E)) }$
261    sout | label(e);
262}
263\end{cfa}
264The shorthand syntax has a type name expression (@Char@ and @E@) as its range. If the range expression does not name
265a \CFA enumeration or a @Serial@, \CFA reports a compile time error. When type name as range is a \CFA enumeration,
266it turns into a loop that iterates all enumerators of the type. If the type name is a @Serial@, the index variable
267will be initialized as the @lowerBound@. The loop control checks the index's position against the position of @upperBound@,
268and terminate the loop when the index has a position greater than the @upperBound@. \CFA does not update the index with
269@succ@ but manipulate its position directly to avoid @out of bound@.
270
271\section{Overload Operators}
272% Finally, there is an associated trait defining comparison operators among enumerators.
273\CFA preemptively overloads comparison operators for \CFA enumeration with @Serial@ and @CfaEnum@.
274They defines that two enumerators are equal only if the are the same enumerator, and compartors are
275define for order comparison.
276\begin{cfa}
277forall( E | CfaEnum( E ) | Serial( E ) ) {
278        // comparison
279        int ?==?( E l, E r );           $\C{// true if l and r are same enumerators}$
280        int ?!=?( E l, E r );           $\C{// true if l and r are different enumerators}$
281        int ?<?( E l, E r );            $\C{// true if l is an enumerator before r}$
282        int ?<=?( E l, E r );           $\C{// true if l before or the same as r}$
283        int ?>?( E l, E r );            $\C{// true if l is an enumerator after r}$
284        int ?>=?( E l, E r );           $\C{// true if l after or the same as r}$
285}
286\end{cfa}
287
288\CFA implements few arithmetic operators for @CfaEnum@. Unlike update functions in @Serial@, these
289operator does not have bound checks, which rely on @upperBound@ and @lowerBound@. These operators directly manipulate
290position, the underlying representation of a \CFA enumeration.
291\begin{cfa}
292forall( E | CfaEnum( E ) | Serial( E ) ) {
293        // comparison
294        E ++?( E & l );
295        E --?( E & l );
296        E ?+=? ( E & l, one_t );
297        E ?-=? ( E & l, one_t );
298        E ?+=? ( E & l, int i );
299        E ?-=? ( E & l, int i );
300        E ?++( E & l );
301        E ?--( E & l );
302}
303\end{cfa}
304
305Lastly, \CFA does not define @zero_t@ for \CFA enumeration. Users can define the boolean false for
306\CFA enumerations on their own. Here is an example:
307\begin{cfa}
308forall(E | CfaEnum(E))
309bool ?!=?(E lhs, zero_t) {
310        return posn(lhs) != 0;
311}
312\end{cfa}
313which effectively turns the first enumeration as a logical false and true for others.
314
315% \begin{cfa}
316% Count variable_a = First, variable_b = Second, variable_c = Third, variable_d = Fourth;
317% p(variable_a); // 0
318% p(variable_b); // 1
319% p(variable_c); // "Third"
320% p(variable_d); // 3
321% \end{cfa}
322
323
324% \section{Iteration and Range}
325
326
327
328% % It is convenient to iterate over a \CFA enumeration value, \eg:
329% \CFA implements \newterm{range loop} for \CFA enumeration using the enumerated traits. The most basic form of @range loop@ is the follows:
330% \begin{cfa}[label=lst:range_functions]
331% for ( Alphabet alph; Alphabet ) { sout | alph; }
332% >>> A B C ... D
333% \end{cfa}
334% % The @range loops@ iterates through all enumerators in the order defined in the enumeration.
335% % @alph@ is the iterating enumeration object, which returns the value of an @Alphabet@ in this context according to the precedence rule.
336% Enumerated @range loop@ extends the \CFA grammar as it allows a type name @Alphabet@
337
338% \textbullet\ \CFA offers a shorthand for iterating all enumeration constants:
339% \begin{cfa}[label=lst:range_functions]
340% for ( Alphabet alph ) { sout | alph; }
341% >>> A B C ... D
342% \end{cfa}
343
344% The following are examples for constructing for-control using an enumeration. Note that the type declaration of the iterating variable is optional, because \CFA can infer the type as EnumInstType based on the range expression, and possibly convert it to one of its attribute types.
345
346% \textbullet\ H is implicit up-to exclusive range [0, H).
347% \begin{cfa}[label=lst:range_function_1]
348% for ( alph; Alphabet.D ) { sout | alph; }
349% >>> A B C
350% \end{cfa}
351
352% \textbullet\ ~= H is implicit up-to inclusive range [0,H].
353% \begin{cfa}[label=lst:range_function_2]
354% for ( alph; ~= Alphabet.D ) { sout | alph; }
355% >>> A B C D
356% \end{cfa}
357
358% \textbullet\ L ~ H is explicit up-to exclusive range [L,H).
359% \begin{cfa}[label=lst:range_function_3]
360% for ( alph; Alphabet.B ~ Alphabet.D  ) { sout | alph; }
361% // for ( Alphabet alph = Alphabet.B; alph < Alphabet.D; alph += 1  ); 1 is one_t
362% >>> B C
363% \end{cfa}
364
365% \textbullet\ L ~= H is explicit up-to inclusive range [L,H].
366% \begin{cfa}[label=lst:range_function_4]
367% for ( alph; Alphabet.B ~= Alphabet.D  ) { sout | alph; }
368% >>> B C D
369% \end{cfa}
370
371% \textbullet\ L -~ H is explicit down-to exclusive range [H,L), where L and H are implicitly interchanged to make the range down-to.
372% \begin{cfa}[label=lst:range_function_5]
373% for ( alph; Alphabet.D -~ Alphabet.B  ) { sout | alph; }
374% >>> D C
375% \end{cfa}
376
377% \textbullet\ L -~= H is explicit down-to exclusive range [H,L], where L and H are implicitly interchanged to make the range down-to.
378% \begin{cfa}[label=lst:range_function_6]
379% for ( alph; Alphabet.D -~= Alphabet.B  ) { sout | alph; }
380% >>> D C B
381% \end{cfa}
382
383% A user can specify the ``step size'' of an iteration. There are two different stepping schemes of enumeration for-loop.
384% \begin{cfa}[label=lst:range_function_stepping]
385% enum(int) Sequence { A = 10, B = 12, C = 14, D = 16, D  = 18 };
386% for ( s; Sequence.A ~= Sequence.D ~ 1  ) { sout | alph; }
387% >>> 10 12 14 16 18
388% for ( s; Sequence.A ~= Sequence.D; s+=1  ) { sout | alph; }
389% >>> 10 11 12 13 14 15 16 17 18
390% \end{cfa}
391% The first syntax is stepping to the next enumeration constant, which is the default stepping scheme if not explicitly specified. The second syntax, on the other hand, is to call @operator+=@ @one_type@ on the @value( s )@. Therefore, the second syntax is equivalent to
392% \begin{cfa}[label=lst:range_function_stepping_converted]
393% for ( typeof( value(Sequence.A) ) s=value( Sequence.A ); s <= Sequence.D; s+=1  ) { sout | alph; }
394% >>> 10 11 12 13 14 15 16 17 18
395% \end{cfa}
396
397% % \PAB{Explain what each loop does.}
398
399% It is also possible to iterate over an enumeration's labels, implicitly or explicitly:
400% \begin{cfa}[label=lst:range_functions_label_implicit]
401% for ( char * alph; Alphabet )
402% \end{cfa}
403% This for-loop implicitly iterates every label of the enumeration, because a label is the only valid resolution to @ch@ with type @char *@ in this case.
404% If the value can also be resolved as the @char *@, you might iterate the labels explicitly with the array iteration.
405% \begin{cfa}[label=lst:range_functions_label_implicit]
406% for ( char * ch; labels( Alphabet ) )
407% \end{cfa}
Note: See TracBrowser for help on using the repository browser.