Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:simply_typed_lambda_calculus [2008/05/27 21:15] vkuncak |
sav08:simply_typed_lambda_calculus [2008/05/27 23:08] vkuncak |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| In simply typed lambda calculus, each variable is assigned one type from $\tau$. | In simply typed lambda calculus, each variable is assigned one type from $\tau$. | ||
| + | |||
| Line 38: | Line 39: | ||
| \end{array}\] | \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 ===== | ||