Changeset 6740533e for doc/theses/jiada_liang_MMath

Timestamp:

Jul 31, 2024, 7:41:21 PM (36 hours ago)

Author:

JiadaL <j82liang@…>

Branches:

master

Children:

3a7cd15

Parents:

21f4dff

Message:

Add a discussion on Static Type information

File:

• doc/theses/jiada_liang_MMath/trait.tex (modified) (1 diff)

doc/theses/jiada_liang_MMath/trait.tex

@@ -97 +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}