Title | Incremental Inference of Partial Types |
Authors | Mario Coppo, UNiversita' di Torino
Daniel Hirschkoff, ENS Lyon |
Main Fields | 7. design of algorithms
9. foundations of functional programming 21. type theory |
Other Main Fields | |
Abstract + Keywords | We present a type inference procedure
for \emph{partial types} for a
$\lambda$--calculus equipped with datatypes. Our procedure handles a type languages containing greatest and lesser types ($\omega$ and $\bot$ respectively), subtyping, and datatypes (yielding constants at the level of terms). The main feature of our algorithm is \emph{incrementality}; this allows us to progressively analyse successive term definitions, which is of interest in the setting of a system like the \textit{CuCh machine} (cuurently being developped at the University of Rome). The methods we describe have led to an implemention; we illustrate its use on a few examples. Ke words: type inference, partial type,
functional languages
|