In the next parts, we will define an algorithmic type system.

In order for it to be complete in regards to lambda-abstractions, we will use a

new syntactic category, called \textbf{type schemes}, that denote a set of types.

In the next parts, we will need an algorithmic type system.

In order for it to be complete in regards to lambda-abstractions, we'll need to use a

new syntactic category, called \textbf{type schemes}, that denotes a set of types.

\[

\begin{array}{lrcl}

...

...

@@ -145,6 +144,7 @@ We use $\Gamma_1,\Gamma_2$ for the type environment obtained by unioning the two

We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we can alpha-rename $\lambda$-abstractions).

Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we define $\typep p \varpi{\Gamma,e,t}$ and $\Gp p {\Gamma,e,t}(\varpi)$ as follows

\\

\mick

{

...

...

@@ -224,8 +224,10 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.\\

\mick{

We define the following algorithmic system. For every (expression, type environment, tests environment) triplet, we deduce a type scheme that represents

the set of types that can be derived. This set has no smallest type in general (that's why we can't deduce a type directly without loosing completeness).

We define the following algorithmic type system. For every (expression, type environment, tests environment) triplet, we can derive an unique type scheme that represents

the set of types that could be derived by a non-deterministic typing system (with subsomption).

This set has no smallest type in general (that's why we need to use type schemes).