Changes in / [1f11818:3a7cd15]

Location:

doc/theses/jiada_liang_MMath

Files:

• background.tex (modified) (1 diff)
• trait.tex (modified) (2 diffs)

doc/theses/jiada_liang_MMath/background.tex

@@ -371 +371 @@
 Calling on type with no mathcing @foo()@ implemented, such as int, causes a compile time type assertion error. 
 
+\subsection{trait}
 A @forall@ clause can asserts on multiple types and with multiple asserting functions. A common practice in \CFA is to group
-the asserting functions in to a named @trait@ . 
+the asserting functions in to a named \newterm{trait}. 
 
 \begin{cfa}

doc/theses/jiada_liang_MMath/trait.tex

@@ -2 +2 @@
 \label{c:trait}
 
+% Despite parametric polymorphism being a pivotal feature of \CFA, for a long time, there was not 
+% a technique to write functions being polymorphic over enumerated types. 
+\CC introduced @std::is_enum@ trait on \CC{11} and @concepts@ on \CC{20}; with the combination, users can 
+write function polymorphic over enumerated type in \CC:
+\begin{cfa}
+#include <type_traits>
+
+template<typename T>
+@concept Enumerable = std::is_enum<T>::value;@
+
+template<@Enumerable@ T>
+void f(T) {}
+\end{cfa}
+The @std::is_enum@ and other \CC @traits@ are a compile-time interfaces to query type information. 
+While named the same as @trait@, it is orthogonal to \CFA trait, as the latter being defined as 
+a collection of assertion to be satisfied by a polymorphic type.
+
+\CFA provides @CfaEnum@ and @TypedEnum@ traits to supports polymorphic functions for \CFA enumeration:
+\begin{cfa}
+forall(T | @CfaEnum(T)@)
+void f(T) {}
+\end{cfa}
+
 \section{CfaEnum and TypedEnum}
-
 \CFA defines attribute functions @label()@ and @posn()@ for all \CFA enumerations, 
 and therefore \CFA enumerations fulfills the type assertions with the combination. 
@@ -75 +97 @@
 \end{cfa}
 
-\subsection{Bounded and Serial}
+\section{Discussion: Static Type Information}
+@CfaEnum@ and @TypedEnum@ are approximations to \CFA Enumerations and Typed Enumerations: they are not 
+assertions on a type being an enumerated type, 
+but rather types being shared an interfaces with \CFA enumerations.
+\CC's @type_traits@ is fundamentally different than \CFA's traits: \CC's @type_traits@ are descriptions 
+of compile time type information
+\footnote{Concepts can check if a \CC class implement a certain method, 
+but it is to probe a static type information of a class having a such member.}
+, while \CFA's trait describe how a type can be used, 
+which is a closer paradigm to a trait system in languages such as Scala and Rust. 
+However, Scala and Rust's traits are nominative: 
+a type explicitly declare a named traits to be of its type; while in \CFA, 
+type implements all functions declares in a trait to implicitly be of the trait type.
+
+If to support static type information, \CFA needs new piece of syntax to distinguish static type 
+query from function calls, for example:
+\begin{cfa}
+forall(T | { T::is_enum; });
+\end{cfa}
+When to call a polymorphic function @foo(T)@ with assertions set @S@ and function call argument @a@, \CFA 
+determines if there is an overloaded name @a@ that has non-zero conversion cost to all assertions in @S@.
+As a consequence, @is_enum@ can be a \CFA directive that immediately trim down the search space of @a@ to 
+be some enumerated types. In fact, because \CFA stores symbols maps to enumeration in a standalone data structure. 
+Limiting search space to enumeration improve on \CFA resolution speed.
+
+While assertion on static type information seems improvement on expressivity, it is a challenge to 
+extend its capability without a fully functional pre-processsor that evaluate constant expression as \CC 
+compilers does. The described @is_enum@ manipulate compiler behaviour, which cannot be easily extended to 
+other usage cases. Therefore, \CFA currently does not support @is_enum@ and utalizes traits as a workaround.
+
+
+\section{Bounded and Serial}
 A bounded type defines a lower bound and a upper bound.
 \begin{cfa}