CODEWITHSUNDEEP
type-inferencelambda-calculus
Ankit Shubham
Ankit Shubham

Reputation: 3619

Well typed and ill typed lambda terms

I have been trying to understand the applied lambda calculus. Up till now, I have understood how type inference works. But I am not able to follow what is the meaning of saying that a term is well-typed or ill-typed and then how can I determine whether a given term is well-typed or ill-typed. For example, consider a lambda term tw defined as λx[(x x)] . How to conclude whether it is a well-typed or ill-typed term?

Upvotes: 1

Views: 2917

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15414

If we are talking about Simply Typed Lambda Calculus with some additional constants and basic types (i.e. applied lambda calculus), then the term λx:σ. (x x) is well-formed, but ill-typed.

'Well-formed' means syntactically correct, i.e. will be accepted by a parser for STLC. 'Ill-typed' means the type-checker would not pass it further. Type-checker works according to the typing rules, which are usually expressed as a number of typing judgements (one typing scheme for each syntactic form).

Let me show that the term you provided is indeed ill-typed. According to the rule (3) [see the typing rules link], λx:σ. (x x) must have type of general form σ -> τ (since it is a function, or more correctly abstraction). But that means the body (x x) must have some type τ (assuming x : σ). This is basically the same rule (3) expressed in a natural language. So, now we need to figure out the type of the function's body, which is an application.

Now, the rule for application (4) says that if we have an expression like this (e1 e2), then e1 must be some function e1 : α -> β and e2 : α must be an argument of the right type. Let's apply this rule to our expression for the body (x x). (1) x : α -> β and (2) x : α. Since an term in STLC can have only one type, we've got an equation: α -> β = α. But there is no way we can unify both types together, since α is a subpart of α -> β. That's why this won't typecheck.

By the way, one of the major points of STLC was to forbid self-application (like (x x)), because it prevents from using (untyped) lambda calculus as a logic, since one can perform non-terminating calculations using self-application (see for instance Y-combinator).

Upvotes: 1

Related Questions