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.
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
©2018 Martin Webb