Index: doc/theses/fangren_yu_MMath/intro.tex =================================================================== --- doc/theses/fangren_yu_MMath/intro.tex (revision 9a1aec6e504a0e5a511cff4a917a51aa7248fee2) +++ doc/theses/fangren_yu_MMath/intro.tex (revision 1e7e6f383fe5f9e7bbf40293a6b9a6f4d470de5b) @@ -30,8 +30,11 @@ \section{Overloading} - +\label{s:Overloading} + +\vspace*{-5pt} \begin{quote} There are only two hard things in Computer Science: cache invalidation and \emph{naming things}. --- Phil Karlton \end{quote} +\vspace*{-5pt} Overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources, like include files. Experience from \CC and \CFA developers shows the type system can implicitly and correctly disambiguate the majority of overloaded names, \ie it is rare to get an incorrect selection or ambiguity, even among hundreds of overloaded (variables and) functions. @@ -39,5 +42,5 @@ Disambiguating among overloads is implemented by examining each call site and selecting the best matching overloaded function based on criteria like the types and number of arguments and the return context. -Since the hardware does not support mixed-mode operands, @2 + 3.5@, the type system must disallow it or (safely) convert the operands to a common type. +Since the hardware does not support mixed-mode operands, such as @2 + 3.5@, the type system must disallow it or (safely) convert the operands to a common type. Like overloading, the majority of mixed-mode conversions are silently resolved, simplifying the development process. This approach matches with programmer intuition and expectation, regardless of any \emph{safety} issues resulting from converted values. @@ -49,12 +52,14 @@ As well, many namespace systems provide a mechanism to open their scope returning to normal overloading, \ie no qualification. While namespace mechanisms are very important and provide a number of crucial program-development features, protection from overloading is overstated. -Similarly, lexical nesting is another place where overloading occurs. +Similarly, lexical nesting is another place where duplicate naming issues arise. For example, in object-oriented programming, class member names \newterm{shadow} names within members. -Some programmers, qualify all member names with @class::@ or @this->@ to make them unique from names defined in members. -Even nested lexical blocks result in shadowing, \eg multiple nested loop-indices called @i@. -Again, coding styles exist requiring all variables in nested block to be unique to prevent name shadowing. +Some programmers qualify all member names with @class::@ or @this->@ to make them unique from names defined in members. +Even nested lexical blocks result in shadowing, \eg multiple nested loop-indices called @i@, silently changing the meaning of @i@ at lower scope levels. +Again, coding styles exist requiring all variables in nested block to be unique to prevent name shadowing problems. Depending on the language, these possible ambiguities can be reported (as warnings or errors) and resolved explicitly using some form of qualification and/or cast. - -Formally, overloading is defined by Strachey as \newterm{ad hoc polymorphism}: +For example, if variables can be overloaded, shadowed variables of different type can produce ambiguities, indicating potential problems in lower scopes. + +Formally, overloading is defined by Strachey as one kind of \newterm{ad hoc polymorphism}: +\vspace*{-5pt} \begin{quote} In ad hoc polymorphism there is no single systematic way of determining the type of the result from the type of the arguments. @@ -63,5 +68,7 @@ It seems, moreover, that the automatic insertion of transfer functions by the compiling system is limited to this.~\cite[p.~37]{Strachey00} \end{quote} +\vspace*{-5pt} where a \newterm{transfer function} is an implicit conversion to help find a matching overload: +\vspace*{-5pt} \begin{quote} The problem of dealing with polymorphic operators is complicated by the fact that the range of types sometimes overlap. @@ -69,4 +76,5 @@ The functions which perform this operation are known as transfer functions and may either be used explicitly by the programmer, or, in some systems, inserted automatically by the compiling system.~\cite[p.~35]{Strachey00} \end{quote} +\vspace*{-5pt} The differentiating characteristic between parametric polymorphism and overloading is often stated as: polymorphic functions use one algorithm to operate on arguments of many different types, whereas overloaded functions use a different algorithm for each type of argument. A similar differentiation is applicable for overloading and default parameters. @@ -128,5 +136,5 @@ \end{cfa} the overloaded names @S@ and @E@ are separated into the type and object domain, and C uses the type kinds @struct@ and @enum@ to disambiguate the names. -In general, types are not overloaded because inferencing them is difficult to imagine in a statically programming language. +In general, types are not overloaded because inferencing them is difficult to imagine in a statically typed programming language. \begin{cquote} \setlength{\tabcolsep}{26pt} @@ -181,5 +189,5 @@ \noindent \newterm{General overloading} occurs when the type-system \emph{knows} a function's parameters and return types (or a variable's type for variable overloading). -In functional programming-languages, there is always a return type (except for a monad). +In functional programming-languages, there is always a return type. If a return type is specified, the compiler does not have to inference the function body. For example, the compiler has complete knowledge about builtin types and their overloaded arithmetic operators. @@ -214,7 +222,10 @@ Hence, parametric overloading requires additional information about the universal types to make them useful. -This additional information often comes as a set of operations a type must supply (@trait@/-@concept@) and these operations can then be used in the body of the function. -\begin{cfa} -forall( T | T ?@++@( T, T ) ) T inc( T t ) { return t@++@; } +This additional information often comes as a set of operations that must be supply for a type, \eg \CFA/Rust/Go have traits, \CC template has concepts, Haskell has type-classes. +These operations can then be used in the body of the function to manipulate the type's value. +Here, a type binding to @T@ must have available a @++@ operation with the specified signature. +\begin{cfa} +forall( T | @T ?++( T, T )@ ) // trait +T inc( T t ) { return t@++@; } // change type value int i = 3 i = inc( i ) @@ -222,5 +233,5 @@ \end{cfa} Given a qualifying trait, are its elements inferred or declared? -In the above example, the type system infers @int@ for @T@, infers it needs a @++@ operator that takes an @int@ and returns an @int@, and finds this function in the enclosing environment (\eg standard prelude). +In the example, the type system infers @int@ for @T@, infers it needs an appropriately typed @++@ operator, and finds it in the enclosing environment, possibly in the language's prelude defining basic types and their operations. This implicit inferencing is expensive if matched with implicit conversions when there is no exact match. Alternatively, types opt-in to traits via declarations. @@ -420,5 +431,5 @@ \subsection{Operator Overloading} -Virtually all programming languages provide general overloading of the arithmetic operators across the basic computational types using the number and type of parameters and returns. +Many programming languages provide general overloading of the arithmetic operators~\cite{OperOverloading} across the basic computational types using the number and type of parameters and returns. However, in some languages, arithmetic operators may not be first class, and hence, cannot be overloaded. Like \CC, \CFA allows general operator overloading for user-defined types. @@ -438,5 +449,6 @@ \subsection{Function Overloading} -Both \CFA and \CC allow general overloading for functions, as long as their prototypes differ in the number and type of parameters and returns. +Many programming languages provide general overloading for functions~\cite{FuncOverloading}, as long as their prototypes differ in the number and type of parameters. +A few programming languages also use the return type for selecting overloaded functions \see{below}. \begin{cfa} void f( void ); $\C[2in]{// (1): no parameter}$ @@ -478,5 +490,5 @@ \begin{cfa} void foo( double d ); -int v; $\C[2in]{// (1)}$ +int v; $\C[2in]{// (1)}$ double v; $\C{// (2) variable overloading}$ foo( v ); $\C{// select (2)}$ @@ -487,5 +499,5 @@ } \end{cfa} -It is interesting that shadow overloading is considered a normal programming-language feature with only slight software-engineering problems. +It is interesting that shadowing \see{namespace pollution in \VRef{s:Overloading}} is considered a normal programming-language feature with only slight software-engineering problems. However, variable overloading within a scope is often considered dangerous, without any evidence to corroborate this claim. In contrast, function overloading in \CC occurs silently within the global scope from @#include@ files all the time without problems. @@ -554,5 +566,5 @@ The following covers these issues, and why this scheme is not amenable with the \CFA type system. -One of the first and powerful type-inferencing system is Hindley--Milner~\cite{Damas82}. +One of the first and most powerful type-inferencing systems is Hindley--Milner~\cite{Damas82}. Here, the type resolver starts with the types of the program constants used for initialization and these constant types flow throughout the program, setting all variable and expression types. \begin{cfa} @@ -579,5 +591,5 @@ Note, return-type inferencing goes in the opposite direction to Hindley--Milner: knowing the type of the result and flowing back through an expression to help select the best possible overloads, and possibly converting the constants for a best match. -In simpler type-inferencing systems, such as C/\CC/\CFA, there are more specific usages. +There are multiple ways to indirectly specify a variable's type, \eg from a prior variable or expression. \begin{cquote} \setlength{\tabcolsep}{10pt} @@ -606,5 +618,6 @@ \end{tabular} \end{cquote} -The two important capabilities are: +Here, @type(expr)@ computes the same type as @auto@ righ-hand expression. +The advantages are: \begin{itemize}[topsep=0pt] \item @@ -616,5 +629,5 @@ This issue is exaggerated with \CC templates, where type names are 100s of characters long, resulting in unreadable error messages. \item -Ensuring the type of secondary variables, match a primary variable. +Ensuring the type of secondary variables match a primary variable. \begin{cfa} int x; $\C{// primary variable}$ @@ -625,4 +638,7 @@ \end{itemize} Note, the use of @typeof@ is more restrictive, and possibly safer, than general type-inferencing. +\begin{cquote} +\setlength{\tabcolsep}{20pt} +\begin{tabular}{@{}ll@{}} \begin{cfa} int x; @@ -630,10 +646,18 @@ type(x) z = ... // complex expression \end{cfa} -Here, the types of @y@ and @z@ are fixed (branded), whereas with type inferencing, the types of @y@ and @z@ are potentially unknown. +& +\begin{cfa} +int x; +auto y = ... // complex expression +auto z = ... // complex expression +\end{cfa} +\end{tabular} +\end{cquote} +On the left, the types of @y@ and @z@ are fixed (branded), whereas on the right, the types of @y@ and @z@ can fluctuate. \subsection{Type-Inferencing Issues} -Each kind of type-inferencing system has its own set of issues that flow onto the programmer in the form of convenience, restrictions, or confusions. +Each kind of type-inferencing system has its own set of issues that affect the programmer in the form of convenience, restrictions, or confusions. A convenience is having the compiler use its overarching program knowledge to select the best type for each variable based on some notion of \emph{best}, which simplifies the programming experience. @@ -657,5 +681,5 @@ As a result, understanding and changing the code becomes almost impossible. Types provide important clues as to the behaviour of the code, and correspondingly to correctly change or add new code. -In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on a fancy IDE that can re-engineer types for them. +In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on an IDE that can re-engineer types for them. For example, given: \begin{cfa} @@ -670,14 +694,12 @@ In this situation, having the type name or its short alias is essential. -\CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint the right types within an expression. +\CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint correct types within an expression. Type inferencing defeats this goal because there is no left-hand type. -Fundamentally, type inferencing tries to magic away variable types from the programmer. -However, this results in lazy programming with the potential for poor performance and safety concerns. -Types are as important as control-flow in writing a good program, and should not be masked, even if it requires the programmer to think! -A similar issue is garbage collection, where storage management is magicked away, often resulting in poor program design and performance.\footnote{ -There are full-time Java consultants, who are hired to find memory-management problems in large Java programs.} -The entire area of Computer-Science data-structures is obsessed with time and space, and that obsession should continue into regular programming. -Understanding space and time issues is an essential part of the programming craft. -Given @typedef@ and @typeof@ in \CFA, and the strong desire to use the left-hand type in resolution, the decision was made not to support implicit type-inferencing in the type system. +Fundamentally, type inferencing tries to remove explicit typing from programming. +However, writing down types is an important aspect of good programming, as it provides a check of the programmer's expected type and the actual type. +Thinking carefully about types is similar to thinking carefully about date structures, often resulting in better performance and safety. +Similarly, thinking carefully about storage management in unmanaged languages is an important aspect of good programming, versus implicit storage management (garbage collection) in managed language.\footnote{ +There are full-time Java consultants, who are hired to find memory-management problems in large Java programs, \eg Monika Beckworth.} +Given @typedef@ and @typeof@, and the strong desire to use the left-hand type in resolution, no attempt has been made in \CFA to support implicit type-inferencing. Should a significant need arise, this decision can be revisited. @@ -702,5 +724,5 @@ int i, * ip = identity( &i ); \end{cfa} -Unlike \CC template functions, \CFA polymorphic functions are compatible with C \emph{separate compilation}, preventing compilation and code bloat. +Unlike \CC template functions, \CFA polymorphic functions are compatible with \emph{separate compilation}, preventing compilation and code bloat. To constrain polymorphic types, \CFA uses \newterm{type assertions}~\cite[pp.~37-44]{Alphard} to provide further type information, where type assertions may be variable or function declarations that depend on a polymorphic type variable. @@ -710,5 +732,5 @@ int val = twice( twice( 3 ) ); $\C{// val == 12}$ \end{cfa} -Parametric polymorphism and assertions occur in existing type-unsafe (@void *@) C functions, like @qsort@ for sorting an array of unknown values. +The closest approximation to parametric polymorphism and assertions in C is type-unsafe (@void *@) functions, like @qsort@ for sorting an array of unknown values. \begin{cfa} void qsort( void * base, size_t nmemb, size_t size, int (*cmp)( const void *, const void * ) ); @@ -761,5 +783,5 @@ The @sized@ assertion passes size and alignment as a data object has no implicit assertions. Both assertions are used in @malloc@ via @sizeof@ and @_Alignof@. -In practise, this polymorphic @malloc@ is unwrapped by the C compiler and the @if@ statement is elided producing a type-safe call to @malloc@ or @memalign@. +In practice, this polymorphic @malloc@ is unwrapped by the C compiler and the @if@ statement is elided producing a type-safe call to @malloc@ or @memalign@. This mechanism is used to construct type-safe wrapper-libraries condensing hundreds of existing C functions into tens of \CFA overloaded functions. @@ -787,7 +809,7 @@ forall( T @| sumable( T )@ ) // use trait T sum( T a[$\,$], size_t size ) { - @T@ total = 0; // initialize by 0 constructor + @T@ total = 0; // initialize by 0 constructor for ( i; size ) - total @+=@ a[i]; // select appropriate + + total @+=@ a[i]; // select appropriate + return total; } @@ -821,10 +843,16 @@ Write bespoke data structures for each context. While this approach is flexible and supports integration with the C type checker and tooling, it is tedious and error prone, especially for more complex data structures. + \item Use @void *@-based polymorphism, \eg the C standard library functions @bsearch@ and @qsort@, which allow for the reuse of code with common functionality. However, this approach eliminates the type checker's ability to ensure argument types are properly matched, often requiring a number of extra function parameters, pointer indirection, and dynamic allocation that is otherwise unnecessary. + \item -Use preprocessor macros, similar to \CC @templates@, to generate code that is both generic and type checked, but errors may be difficult to interpret. -Furthermore, writing and using complex preprocessor macros is difficult and inflexible. +Use an internal macro capability, like \CC @templates@, to generate code that is both generic and type checked, but errors may be difficult to interpret. +Furthermore, writing complex template macros is difficult and complex. + +\item +Use an external macro capability, like M4~\cite{M4}, to generate code that is generic code, but errors may be difficult to interpret. +Like internal macros, writing and using external macros is equally difficult and complex. \end{enumerate} @@ -903,5 +931,5 @@ general\footnote{overloadable entities: V $\Rightarrow$ variable, O $\Rightarrow$ operator, F $\Rightarrow$ function, M $\Rightarrow$ member} & O\footnote{except assignment}/F & O/F/M & V/O/F & M\footnote{not universal} & O/M & O/F/M & no & no \\ -general constraints\footnote{T $\Rightarrow$ parameter type, \# $\Rightarrow$ parameter number, N $\Rightarrow$ parameter name; R $\Rightarrow$ return type} +general constraints\footnote{T $\Rightarrow$ parameter type, \# $\Rightarrow$ parameter count, N $\Rightarrow$ parameter name; R $\Rightarrow$ return type} & T/\#//R\footnote{parameter names can be used to disambiguate among overloads but not create overloads} & T/\# & T/\#/R & T/\# & T/\#/N/R & T/\#/N/R & T/\#/N & T/R \\ @@ -1000,5 +1028,5 @@ However, the parameter operations are severely restricted because universal types have few operations. -For example, swift provides a @print@ operation for its universal type, and the java @Object@ class provides general methods: @toString@, @hashCode@, @equals@, @finalize@, \etc. +For example, Swift provides a @print@ operation for its universal type, and the Java @Object@ class provides general methods: @toString@, @hashCode@, @equals@, @finalize@, \etc. This restricted mechanism still supports a few useful functions, where the parameters are abstract entities, \eg: \begin{swift} @@ -1031,5 +1059,5 @@ \begin{figure} -\setlength{\tabcolsep}{15pt} +\setlength{\tabcolsep}{12pt} \begin{tabular}{@{}ll@{}} \multicolumn{1}{c}{\textbf{\CFA}} & \multicolumn{1}{c}{\textbf{Haskell}} \\ @@ -1037,12 +1065,10 @@ forall( T ) trait sumable { void ?{}( T &, zero_t ); - T ?+=?( T &, T ); -}; + T ?+=?( T &, T ); }; forall( T | sumable( T ) ) T sum( T a[], size_t size ) { T total = 0; for ( i; size ) total += a[i]; - return total; -} + return total; } struct S { int i, j; }; void ?{}( S & s, zero_t ) { s.[i, j] = 0; } @@ -1050,13 +1076,11 @@ void ?{}( S & s, int i, int j ) { s.[i, j] = [i, j]; } S ?+=?( S & l, S r ) { l.[i, j] += r.[i, j]; } - -int main() { - int ia[] = { 1, 2, 3 }; - sout | sum( ia, 3 ); // trait inference - double da[] = { 1.5, 2.5, 3.5 }; - sout | sum( da, 3 ); // trait inference - S sa[] = { {1, 1}, {2, 2}, {3, 3 } }; - sout | sum( sa, 3 ).[i, j]; // trait inference -} +int main() { // trait inferencing + sout | sum( (int []){ 1, 2, 3 }, 3 ); + sout | sum( (double []){ 1.5, 2.5, 3.5 }, 3 ); + sout | sum( (S []){ {1,1}, {2,2}, {3,3} }, 3 ).[i, j]; } + + + \end{cfa} & @@ -1065,11 +1089,7 @@ szero :: a sadd :: a -> a -> a - ssum :: Sumable a $=>$ [a] -> a ssum (x:xs) = sadd x (ssum xs) ssum [] = szero - - - data S = S Int Int deriving Show @instance Sumable Int@ where @@ -1078,5 +1098,5 @@ @instance Sumable Float@ where szero = 0.0 - sadd = (+) + sadd = (+) @instance Sumable S@ where szero = S 0 0 @@ -1088,10 +1108,10 @@ \end{haskell} \end{tabular} -\caption{Implicitly/Explicitly Trait Inferencing} -\label{f:ImplicitlyExplicitlyTraitInferencing} +\caption{Implicit/Explicit Trait Inferencing} +\label{f:ImplicitExplicitTraitInferencing} \end{figure} One differentiating feature among these specialization techniques is the ability to implicitly or explicitly infer the trait information at a class site. -\VRef[Figure]{f:ImplicitlyExplicitlyTraitInferencing} compares the @sumable@ trait and polymorphic @sum@ function \see{\VRef{s:Traits}} for \CFA and Haskell. +\VRef[Figure]{f:ImplicitExplicitTraitInferencing} compares the @sumable@ trait and polymorphic @sum@ function \see{\VRef{s:Traits}} for \CFA and Haskell. Here, the \CFA type system inferences the trait functions at each call site, so no additional specification is necessary by the programmer. The Haskell program requires the programmer to explicitly bind the trait and to each type that can be summed. @@ -1103,5 +1123,5 @@ \end{ada} Finally, there is a belief that certain type systems cannot support general overloading, \eg Haskell. -As \VRef[Table]{t:OverloadingFeatures} shows, there are multiple languages with both general and parametric overloading, so the decision to not support general overloading is based on the opinion of the language designers and the type system they choose, not any reason in type theory. +As \VRef[Table]{t:OverloadingFeatures} shows, there are multiple languages with both general and parametric overloading, so the decision to not support general overloading is based on design choices made by the language designers not any reason in type theory. The fourth row classifies if conversions are attempted beyond exact match. @@ -1122,5 +1142,5 @@ The details of compiler optimization work are covered in a previous technical report~\cite{Yu20}, which essentially forms part of this thesis. \item -The thesis presents a systematic review of the new features added to the \CFA language and its type system. +This thesis presents a systematic review of the new features added to the \CFA language and its type system. Some of the more recent inclusions to \CFA, such as tuples and generic structure types, were not well tested during development due to the limitation of compiler performance. Several issues coming from the interactions of various language features are identified and discussed in this thesis;