Changeset 6740533e


Ignore:
Timestamp:
Jul 31, 2024, 7:41:21 PM (3 months ago)
Author:
JiadaL <j82liang@…>
Branches:
master
Children:
3a7cd15
Parents:
21f4dff
Message:

Add a discussion on Static Type information

File:
1 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/jiada_liang_MMath/trait.tex

    r21f4dff r6740533e  
    9797\end{cfa}
    9898
    99 \subsection{Bounded and Serial}
     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}
    100131A bounded type defines a lower bound and a upper bound.
    101132\begin{cfa}
Note: See TracChangeset for help on using the changeset viewer.