Differences

This shows you the differences between two versions of the page.

--- sav08:simply_typed_lambda_calculus [2008/05/27 21:15]
vkuncak
+++ sav08:simply_typed_lambda_calculus [2008/05/27 23:14]
vkuncak
@@ Line 16: / Line 16: @@
 In simply typed lambda calculus, each variable is assigned one type from $\tau$.
@@ Line 38: / Line 39: @@
 \end{array}\]
-Note that there is no way to annotate e.g. term $\lambda x. x x$ to have concrete types in the simply typed system.
+Note that there is no way to assign a type to $x$ such that the term $\lambda x. x x$ is well typed.  Therefore, $\lambda x.xx$ is not a term of simply typed lambda calculus.
 ===== Hindley-Milner Type Inference =====
-Hindley-Milner type inference uses unification to infer possible types of lambda terms, even if we do not specify types for variables.  In some cases, such as $\lambda x.x$, there is an infinite family of possible concrete types.  In such cases, Hindley-Milner inference computes the most-general unifier of constraints, which gives polymorphic type.  For simplicity we assume that we have obtained some concrete types for variables and therefore for lambda terms.
+Hindley-Milner type inference uses unification to infer possible types of lambda terms, even if we do not specify types for variables.  The problem reduces to unification in language that has as many constants as there are base types, and one binary constructor (function constructor).
+In some cases, such as $\lambda x.x$, there is an infinite family of possible concrete types.  In such cases, Hindley-Milner inference computes the most-general unifier of constraints, which gives polymorphic type.  For simplicity we assume that we have obtained some concrete types for variables and therefore for lambda terms.
 ===== Strong Normalization =====