Changeset 1c2c253

Mar 22, 2017, 1:25:15 PM (5 years ago)
Aaron Moss <a3moss@…>
aaron-thesis, arm-eh, cleanup-dtors, deferred_resn, demangler, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, new-env, no_list, persistent-indexer, resolv-new, with_gc
06ccbc7, c2bfb31

Added polymorphic functions and traits background to generic types paper from comp II submission, also make CFA code formatting work

1 edited


  • doc/generic_types/generic_types.tex

    ra53e10a r1c2c253  
     1% take of review (for line numbers) and anonymous (for anonymization) on submission
    12\documentclass[format=acmlarge, anonymous, review]{acmart}
     4\usepackage{listings}   % For code listings
     6% Useful macros
     7\newcommand{\CFA}{C$\mathbf\forall$} % Cforall symbolic name
     8\newcommand{\CC}{\rm C\kern-.1em\hbox{+\kern-.25em+}} % C++ symbolic name
     9\newcommand{\CCeleven}{\rm C\kern-.1em\hbox{+\kern-.25em+}11} % C++11 symbolic name
     10\newcommand{\CCfourteen}{\rm C\kern-.1em\hbox{+\kern-.25em+}14} % C++14 symbolic name
     11\newcommand{\CCseventeen}{\rm C\kern-.1em\hbox{+\kern-.25em+}17} % C++17 symbolic name
     18% CFA programming language, based on ANSI C (with some gcc additions)
     20        morekeywords={_Alignas,_Alignof,__alignof,__alignof__,asm,__asm,__asm__,_At,_Atomic,__attribute,__attribute__,auto,
     21                _Bool,catch,catchResume,choose,_Complex,__complex,__complex__,__const,__const__,disable,dtype,enable,__extension__,
     22                fallthrough,fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,__label__,lvalue,_Noreturn,one_t,otype,restrict,_Static_assert,
     23                _Thread_local,throw,throwResume,trait,try,typeof,__typeof,__typeof__,zero_t},
     29basicstyle=\linespread{0.9}\sf,                                                 % reduce line spacing and use sanserif font
     30stringstyle=\tt,                                                                                % use typewriter font
     31tabsize=4,                                                                                              % 4 space tabbing
     32xleftmargin=\parindent,                                                                 % indent code to paragraph indentation
     33% extendedchars=true,                                                                   % allow ASCII characters in the range 128-255
     34% escapechar=§,                                                                                 % LaTeX escape in CFA code §...§ (section symbol), emacs: C-q M-'
     35mathescape=true,                                                                                % LaTeX math escape in CFA code $...$
     36keepspaces=true,                                                                                %
     37showstringspaces=false,                                                                 % do not show spaces with cup
     38showlines=true,                                                                                 % show blank lines at end of code
     39aboveskip=4pt,                                                                                  % spacing above/below code block
     41% replace/adjust listing characters that look bad in sanserif
     42literate={-}{\raisebox{-0.15ex}{\texttt{-}}}1 {^}{\raisebox{0.6ex}{$\scriptscriptstyle\land\,$}}1
     43        {~}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}}1 {_}{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}1 {`}{\ttfamily\upshape\hspace*{-0.1ex}`}1
     44        {<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2,
     45% moredelim=**[is][\color{red}]{®}{®},                                  % red highlighting ®...® (registered trademark symbol) emacs: C-q M-.
     46% moredelim=**[is][\color{blue}]{ß}{ß},                                 % blue highlighting ß...ß (sharp s symbol) emacs: C-q M-_
     47% moredelim=**[is][\color{OliveGreen}]{¢}{¢},                   % green highlighting ¢...¢ (cent symbol) emacs: C-q M-"
     48% moredelim=[is][\lstset{keywords={}}]{¶}{¶},                   % keyword escape ¶...¶ (pilcrow symbol) emacs: C-q M-^
     49}% lstset
     51% inline code @...@
     54% ACM Information
    5 \newcommand{\CFA}{C$\mathbf\forall$}
    6 \newcommand{\TODO}{\textbf{TODO}}
    4998\ccsdesc[300]{Software and its engineering~Source code generation}
    51 % \abstract{Abstract goes here.}
    53101\TODO{} Write abstract.
    60108\section{Introduction \& Background}
    61 \CFA{}\footnote{Pronounced ``C-for-all'', and written \CFA{} or Cforall.} is an evolutionary modernization of the C programming language which aims to add modern language features to C while maintaining both source compatibility with C and a familiar mental model for programmers. This paper describes how generic types are designed and implemented in \CFA{}, and how they interact with \CFA{}'s polymorphic functions.
    63 \CFA{}'s polymorphism was originally formalized by \citet{Ditchfield92}, and first implemented by \citet{Bilson03}.
     110\CFA{}\footnote{Pronounced ``C-for-all'', and written \CFA{} or Cforall.} is an evolutionary extension of the C programming language which aims to add modern language features to C while maintaining both source compatibility with C and a familiar mental model for programmers. This paper describes how generic types are designed and implemented in \CFA{}, and how they interact with \CFA{}'s polymorphic functions.
     112\subsection{Polymorphic Functions}
     114\CFA{}'s polymorphism was originally formalized by \citet{Ditchfield92}, and first implemented by \citet{Bilson03}. The signature feature of \CFA{} is parametric-polymorphic functions; such functions are written using a @forall@ clause (which gives the language its name):
     116forall(otype T)
     117T identity(T x) {
     118    return x;
     121int forty_two = identity(42); // T is bound to int, forty_two == 42
     123The @identity@ function above can be applied to any complete object type (or ``@otype@''). The type variable @T@ is transformed into a set of additional implicit parameters to @identity@, which encode sufficient information about @T@ to create and return a variable of that type. The \CFA{} implementation passes the size and alignment of the type represented by an @otype@ parameter, as well as an assignment operator, constructor, copy constructor and destructor. Here, the runtime cost of polymorphism is spread over each polymorphic call, due to passing more arguments to polymorphic functions; preliminary experiments have shown this overhead to be similar to \CC{} virtual function calls.
     125Since bare polymorphic types do not provide a great range of available operations, \CFA{} provides a \emph{type assertion} mechanism to provide further information about a type:
     127forall(otype T | { T twice(T); })
     128T four_times(T x) {
     129    return twice( twice(x) );
     132double twice(double d) { return d * 2.0; } // (1)
     134double magic = four_times(10.5); // T is bound to double, uses (1) to satisfy type assertion
     136These type assertions may be either variable or function declarations that depend on a polymorphic type variable. @four_times@ can only be called with an argument for which there exists a function named @twice@ that can take that argument and return another value of the same type; a pointer to the appropriate @twice@ function is passed as an additional implicit parameter to the call of @four_times@.
     138Monomorphic specializations of polymorphic functions can themselves be used to satisfy type assertions. For instance, @twice@ could have been defined using the \CFA{} syntax for operator overloading as:
     140forall(otype S | { S ?+?(S, S); })
     141S twice(S x) { return x + x; }  // (2)
     143This version of @twice@ works for any type @S@ that has an addition operator defined for it, and it could have been used to satisfy the type assertion on @four_times@.
     144The compiler accomplishes this by creating a wrapper function calling @twice // (2)@ with @S@ bound to @double@, then providing this wrapper function to @four_times@\footnote{\lstinline@twice // (2)@ could also have had a type parameter named \lstinline@T@; \CFA{} specifies renaming of the type parameters, which would avoid the name conflict with the type variable \lstinline@T@ of \lstinline@four_times@.}.
     148\CFA{} provides \emph{traits} as a means to name a group of type assertions, as in the example below:
     150trait has_magnitude(otype T) {
     151    bool ?<?(T, T);  // comparison operator for T
     152    T -?(T);  // negation operator for T
     153    void ?{}(T*, zero_t);  // constructor from 0 literal
     156forall(otype M | has_magnitude(M))
     157M abs( M m ) {
     158    M zero = { 0 };  // uses zero_t constructor from trait
     159    return m < zero ? -m : m;
     162forall(otype M | has_magnitude(M))
     163M max_magnitude( M a, M b ) {
     164    return abs(a) < abs(b) ? b : a;
     168Semantically, traits are simply a named lists of type assertions, but they may be used for many of the same purposes that interfaces in Java or abstract base classes in \CC{} are used for. Unlike Java interfaces or \CC{} base classes, \CFA{} types do not explicitly state any inheritance relationship to traits they satisfy; this can be considered a form of structural inheritance, similar to implementation of an interface in Go, as opposed to the nominal inheritance model of Java and \CC{}. Nominal inheritance can be simulated with traits using marker variables or functions:
     170trait nominal(otype T) {
     171    T is_nominal;
     174int is_nominal;  // int now satisfies the nominal trait
     176    char is_nominal; // char satisfies the nominal trait
     178// char no longer satisfies the nominal trait here 
     181Traits, however, are significantly more powerful than nominal-inheritance interfaces; firstly, due to the scoping rules of the declarations that satisfy a trait's type assertions, a type may not satisfy a trait everywhere that the type is declared, as with @char@ and the @nominal@ trait above. Secondly, traits may be used to declare a relationship among multiple types, a property that may be difficult or impossible to represent in nominal-inheritance type systems:
     183trait pointer_like(otype Ptr, otype El) {
     184    lvalue El *?(Ptr); // Ptr can be dereferenced into a modifiable value of type El
     187struct list {
     188    int value;
     189    list *next;  // may omit "struct" on type names
     192typedef list *list_iterator;
     194lvalue int *?( list_iterator it ) {
     195    return it->value;
     199In the example above, @(list_iterator, int)@ satisfies @pointer_like@ by the user-defined dereference function, and @(list_iterator, list)@ also satisfies @pointer_like@ by the built-in dereference operator for pointers. Given a declaration @list_iterator it@, @*it@ can be either an @int@ or a @list@, with the meaning disambiguated by context (\eg, @int x = *it;@ interprets @*it@ as an @int@, while @(*it).value = 42;@ interprets @*it@ as a @list@).
     200While a nominal-inheritance system with associated types could model one of those two relationships by making @El@ an associated type of @Ptr@ in the @pointer_like@ implementation, few such systems could model both relationships simultaneously.
Note: See TracChangeset for help on using the changeset viewer.