Ignore:
Timestamp:
Apr 25, 2019, 2:23:48 PM (3 years ago)
Author:
Aaron Moss <a3moss@…>
Branches:
aaron-thesis, arm-eh, cleanup-dtors, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr
Children:
98b4b12
Parents:
69c37cc
Message:

thesis: apply round 2 revisions and strip change bars

File:
1 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/aaron_moss_PhD/phd/introduction.tex

    r69c37cc rf845e80  
    3737\end{itemize}
    3838
    39 \cbstart
    4039The prototype system, which implements the algorithmic contributions of this thesis, is the first performant type-checker implementation for a \CFA{}-style type system.
    4140As the existence of an efficient compiler is necessary for the practical viability of a programming language, the contributions of this thesis comprise a validation of the \CFA{} language design that was previously lacking.
    42 \cbend
    4341
    4442Though the direction and experimental validation of this work is fairly narrowly focused on the \CFA{} programming language, the tools used and results obtained should be of interest to a wider compiler and programming language design community.
    4543In particular, with the addition of \emph{concepts} in \CCtwenty{}~\cite{C++Concepts}, conforming \CC{} compilers must support a model of type assertions very similar to that in \CFA{}, and the algorithmic techniques used here may prove useful.
    46 \cbstart
    47 Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow type inference from the context of a function call in addition to its arguments; this feature allows the programmers to specify fewer redundant type annotations on functions that are polymorphic in their return type.
    48 \cbend \cbstartx
    49 The !auto! keyword in \CCeleven{} supports a similar but sharply restricted form of this contextual inference -- the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of \CC{}.
    50 By contrast, Java~8~\cite{Java8} and Scala~\cite{Scala} use comparably powerful forms of type inference, so the algorithmic techniques in this thesis may be effective for those languages' compiler implementors.
    51 \cbendx
     44Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow overload selection from the context of a function call based on function return type in addition to the type of the arguments to the call; this feature allows the programmers to specify fewer redundant type annotations on functions that are polymorphic in their return type.
     45As an example in \CC{}:
     46\begin{C++}
     47template<typename T> T* zero() { return new T( 0 ); }
     48
     49int* z = zero<int>();  $\C{// must specify int twice}$
     50\end{C++}
     51
     52\CFA{} allows !int* z = zero()!, which elides the second !int!.
     53While the !auto! keyword in \CCeleven{} supports similar inference in a limited set of contexts (\eg{} !auto z = zero<int>()!), the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of \CC{}.
     54By contrast to \CC{}, Java~8~\cite{Java8} and Scala~\cite{Scala} use comparably powerful forms of type inference to \CFA{}, so the algorithmic techniques in this thesis may be effective for those languages' compiler implementors.
    5255Type environments are also widely modelled in compiler implementations, particularly for functional languages, though also increasingly commonly for other languages (such as Rust~\cite{Rust}) that perform type inference; the type environment presented here may be useful to those language implementors.
    5356
    54 \cbstarty
    5557One area of inquiry that is outside the scope of this thesis is formalization of the \CFA{} type system.
    56 Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system.
     58Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus, which is the theoretical basis for the \CFA{} type system.
    5759Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work.
    5860A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}.
    59 One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types that are conceptually similar to \CFA{} traits.
     61One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types that is conceptually similar to \CFA{} traits.
    6062These modelling approaches could potentially be used to extend an existing formal semantics for C such as Cholera \cite{Norrish98}, CompCert \cite{Leroy09}, or Formalin \cite{Krebbers14}.
    61 \cbendy
Note: See TracChangeset for help on using the changeset viewer.