Consider the typing judgement:
where has the form
The derivation of this judgement using Curry's scheme takes the
untyped term and derives a type for it. This method is polymorphic.
In Gunter's text the method used is Church's scheme, which takes
tagged
-terms, eg
.
ML appears to use Curry types because of the type inference mechanism, but in fact Church's scheme is used in the raw syntax of the language (in spite of the polymorphism).
The problem of type checking is to determine given whether
. We do this by trying to build a derivation
(ie a proof).
Type inference is the problem of finding such that
, given
. Algorithm
, used in ML is an example of
type inference.
Type inhabitation, or program synthesis, is finding a program
such that
, given
.