Changeset 6174ecc

Timestamp:

Apr 9, 2025, 9:43:41 PM (5 months ago)

Author:

Michael Brooks <mlbrooks@…>

Branches:

master

Children:

b1b513d

Parents:

119889f (diff), d914750 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' of plg.uwaterloo.ca:software/cfa/cfa-cc

Location:

doc/theses/fangren_yu_MMath

Files:

• background.tex (modified) (2 diffs)
• resolution.tex (modified) (1 diff)
• uw-ethesis.tex (modified) (1 diff)

doc/theses/fangren_yu_MMath/background.tex

@@ -1 @@
-\chapter{Background}
+\chapter{Related Work}
 
 \section{Polymorphism}
@@ -66 +66 @@
 Java's variadic functions appear similar to C's but are type safe using homogeneous arrays, which are less useful than \CFA's heterogeneously typed variadic functions.
 Tuples are a fundamental abstraction in most functional programming languages, such as Standard ML~\cite{sml}, Haskell, and Scala~\cite{Scala}, which decompose tuples using pattern matching.
+
+
+\section{Type resolution}
+
+\CFA expression resolution must deal with extensive overloading and inference of polymorphic types with assertions.
+The goal is to keep the base algorithm used in type unification simple enough so resolving a complicated expression can still be done reasonably fast.
+The following is work that handles the aforementioned bidirectional subtyping relations concisely.
+
+Melo~\etal~\cite{Melo17} developed PsycheC, a tool built for inferencing missing type and variable declarations of incomplete C programs, which can also be viewed as a dialect of C with type inferencing.
+As PsycheC is built for analyzing standard C programs, it does not have any kind of overloading or polymorphism.
+Instead, all top-level variables and function parameters may have indeterminate types.
+The scope of the problem PsycheC deals with is quite the opposite of that in \CFA, but the techniques used to solve for the unknown types are similar. 
+
+In PsycheC, a unification variable is assigned to every identifier with unknown type, and each use of a variable generates a constraint on its type.
+Just like in \CFA, the most common kinds of expression contexts PsycheC deals with are assignments and function calls, which creates inequality constraints: the right hand side of the assignment is a subtype of the left hand side;
+function argument passing is treated the same as assignment.
+Since both sides of the inequality can have unknown types, type resolution needs to handle both upper bound and lower bound constraints. 
+Instead of directly solving with lower and upper bounds, the authors developed a two-phase unification algorithm where the equivalences are first resolved and substituted into the inequalities, and showed that by ordering the inequalities using the partial order of concrete types involved, a second pass of unification treating inequalities as equivalences is sufficient to resolve all type variables.
+However, PsycheC does not consider the hierarchy of arithmetic types, as they are all mutually convertible in C, and therefore, considered \emph{equivalent} in unification.
+It also lacks structured types except simple pointers, meaning their strategy of unifying subtypes as equivalences does not work in a more general setting such as in \CFA. 
+
+Pierce and Turner~\cite{Pierce00} presented a \emph{local} type-inference method that restricts the propagation of types and use of unification variables within adjacent syntax-tree nodes.
+The technique provides sufficient type checking and inference for the ML family of languages.
+Odersky, Zenger, and Zenger~\cite{Odersky01} refined this method by introducing a coloured type-system that distinguishes inherited types (given directly by context) and synthesized types (deducted from the term itself), to handle bidirectional type propagation in a more concise manner. 
+Their algorithm is designed for functional programming, where a first-class (untyped) lambda expression is common and type inference must also deduce the argument types of lambdas requiring bidirectional inference. 
+Given that \CFA does not have lambda expressions, but the rest of the type inference cases are quite similar, implementing this type-inference algorithm for \CFA expression resolution might be promising.
+Moreover, the current \CFA implementation also keeps unification variables \emph{almost} local, except when a type variable does not appear in the parameter list.
+Hence, it cannot be given a value from the argument types;
+rather, it is passed upwards as a free variable for matching.
+In all other cases, the substituted minimal types are passed upwards as the result types.
+This process means the current implementation of \CFA expression resolution semantically agrees with Pierce's type-inference system in most of the cases.
+A question remains whether these methods can be adapted to handle \CFA assertion resolution.

doc/theses/fangren_yu_MMath/resolution.tex

@@ -626 +626 @@
 \end{cfa}
 forces the desired type binding, since the cast only compiles when the expression type matches exactly with the target.
-
-\section{Related Work}
-
-\CFA expression resolution may deal with extensive overloading and inference of polymorphic types with assertions, and we want to keep the base algorithm used in type unification simple enough so that resolving a complicated expression can still be done reasonably fast.
-In this section, we look at some related work that handles the aforementioned bidirectional subtyping relations concisely.
-
-Melo, et. al.~\cite{Melo17} developed PsycheC, a tool built for inferencing missing type and variable declarations of incomplete C programs, which can also be viewed as a dialect of C with type inferencing. As PsycheC is built for analyzing standard C programs, it does not have any kind of overloading or polymorphism. Instead, all top-level variables and function parameters may have indeterminate types. The scope of the problem PsycheC deals with is quite the opposite of that in \CFA, but the techniques used to solve for the unknown types are similar. 
-In PsycheC, a unification variable is assigned to every identifier with unknown type, and each use of a variable generates a constraint on its type. Just like in \CFA, the most common kinds of expression contexts PsycheC deals with are assignments and function calls, which creates inequality constraints: the right hand side of the assignment is a subtype of the left hand side; function argument passing is treated the same as assignment. Since both sides of the inequality can have unknown types, type resolution needs to handle both upper bound and lower bound constraints. 
-Instead of directly solving with lower and upper bounds, the authors developed a two-phase unification algorithm where the equivalences are first resolved and substituted into the inequalities, and showed that by ordering the inequalities using the partial order of concrete types involved, a second pass of unification treating inequalities as equivalences will be sufficient to resolve all type variables.
-Note that, however, PsycheC does not consider the hierarchy of arithmetic types, as they are all mutually convertible in C and therefore considered "equivalent" in unification, and it also lacks structured types except simple pointers, meaning this strategy of unifying subtypes as equivalences will not work in a more general setting such as in \CFA. 
-
-Pierce and Turner~\cite{Pierce00} presented a \textit{local} type inference method that restricts the propagation of types and use of unification variables within adjacent syntax tree nodes. The technique is developed to provide sufficient type checking and inference in the ML family of languages. Odersky, Zenger and Zenger~\cite{Odersky01} refined their method by introducing a colored type system which distinguishes inherited types (given directly by context) and synthesized types (deducted from the term itself), to handle bidirectional type propagation in a more concise manner. 
-Their algorithms are designed for functional programming, where first-class (untyped) lambda expressions are common and type inference must also deduce the argument types of lambdas, and hence bidirectional inference must be supported. 
-Given that \CFA does not have lambda expressions, and the rest of type inference cases are quite similar, implementing this type inference algorithm for \CFA expression resolution might be promising. Moreover, the current \CFA implementation also keeps unification variables \textit{almost} local, with the exception that whenever a type variable does not appear in the parameter list and therefore cannot be given a value by the argument types, it is passed upwards as a free variable. In all other cases, the substituted minimal types are passed upwards as the result types. This means that the current implementation of \CFA expression resolution semantically agrees with Pierce's type inference system in most of the cases. A question remains whether these methods can be adapted to handle \CFA assertion resolution.

doc/theses/fangren_yu_MMath/uw-ethesis.tex

@@ -214 +214 @@
 
 \input{intro}
-\input{background}
 \input{features}
 \input{resolution}
+\input{background}
 \input{future}
 \input{conclusion}