@TechReport{ it:2015-038,
author = {Sven-Olof Nystr{\"o}m},
title = {Subtyping and Algebraic Data Types},
institution = {Department of Information Technology, Uppsala University},
department = {Computing Science Division},
year = {2015},
number = {2015-038},
month = dec,
abstract = {We present a new method for type inference. Traditional
approaches rely on an inductively defined domain of types.
Instead, we specify the properties of the type system as a
set of axioms, and give a polynomial-time algorithm for
checking whether there is any domain of types for which the
program types. We show the correctness of the algorithm and
also prove that safety properties are satisfied; any
program accepted by the type system will not cause type
errors at run-time.
The advantages of our approach is that is simpler and more
general. The algorithm for checking that a program types is
a simple mechanism for propagating type information which
should be easy to extend to support other programming
language features. The type checking algorithm is more
general than other approaches as the algorithm will accept
any program that types under any type system that satisfies
the axioms.
We also show how to make type information available to
compilers and other development tools through an algorithm
to determine entailment.
The language we consider is lambda calculus extended with a
constructors and a form of type construct we call
\emph{open case expressions}. Open case expressions allow a
program to manipulate abstract data types where the sets of
constructors overlap.}
}