You are here: irt.org | FOLDOC | typed lambda-calculus
<theory> (TLC) A variety of lambda-calculus in which every term is labelled with a type.
A function application (A B) is only synctactically valid if A has type s --> t, where the type of B is s (or an instance or s in a polymorphic language) and t is any type.
If the types allowed for terms are restricted, e.g. to Hindley-Milner types then no term may be applied to itself, thus avoiding one kind of non-terminating evaluation.
Most functional programming languages, e.g. Haskell, ML, are closely based on variants of the typed lambda-calculus.
(1995-03-25)
Nearby terms: type-ahead search « type assignment « type class « typed lambda-calculus » TypedProlog » typeface » type inference
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL