Type Environment | Exercise 4

A type environment (T) maps variables names to theirs types. For example:

+ is mapped to the type ,  Int -> Int -> Int
y is mapped to the type Int

Lambda Expressions & Types:

Each lambda expression can be typed based on it's structure. The typing rules generally follow:

1. For a variable x of type T, it can be written as x:T

\x:T1.e

1. X is a variable that is bound in the expression e.
2. T1 is the type that you are assigning to x
3. e is the body of the lambda abstraction, which may involve x & potentially other variables.

\x:Int. x + 1

1. X is assumed to have type Int (T1)
2. In the body x + 1, since x is replaced with an Int, the expression to type Int (T2)
3. The type of the lambda abstraction is:
4. Int -> Int

Function Application Typing:

For an application of the form:

(e1 e2)
e1 -> expected to be a function
e2 -> is the arg being passed to this function

Typing Rules:

1. Type of e1: if e1 has a type T1 -> T2, this means e1 is a function that takes an argument of type T1 and returns a value T2.
2. Type of e2: If e2 has a type T1, this means that e2 is an appropriate argument for the function e1.
3. Resulting Type: If both conditions are satisfied, then the whole application (e1 e2) has the type T2.

This indicates that the result of applying the function e1 to the argument e2 will yield a value of type T2.

e1 = \x:Int. x + 1

here e1 has a type Int -> Int

Argument:
e2 = 5, e2 has type int

Application
(e1 e2) -> (\x:Int. x + 1) 5

Since e1 has a type Int -> Int & e2 has type Int, the whole expression (e1 e2) has type Int.

1. What is Γ (Gamma)?

Γ (Gamma), represents a type environment or type context. It is a mapping of variable names to their types.

It keeps tracks of the types of all variables in scope at a given point in your expressions.

Γ = {x:Int, y:Bool}

1. This means variable x has Int
2. Variable y has type Bool

What does x:T mean?

• x:T: This notation means that the variable x has type T.
• In the context of typing rules, when you see x:T in the type environment (Γ), it indicates that x is associated with the type T.

Type Derivation Example

• For each expression, you will derive its type step by step, applying the typing rules based on the given type environment.

We are given:

Γ = {+ → Int → Int → Int, y → Int}

Expression 1

 t1: \x:Int.y + x

• x is of type Int.
• y is also of type Int.
• The expression y + x is valid since both operands are of type Int.
• Type of t1: Int → Int (since it takes an Int and returns an Int).

Expression 2

t2 = \f:Int -> Int.\x:Int.f x

Variable f is defined as a function Int -> Int
Variable x is defined to have Int, 
but the inner function \x:Int.f x, takes x as Int but applies f
i.e (Int -> Int)

thus,
(Int -> Int) -> (Int -> Int)


so t2 is defined as (Int0

• Since f has type Int -> Int & X has type Int,
• applying f to x is valid.
• Applying f to x yields an integer, as f is Int→Int
• T2 is function that takes f (Int -> Int), and return another function (Int -> Int)
• (Int→Int)→(Int→Int)

Expression 3

t3= t2 t1 
(Int -> Int) -> (Int -> Int)  (Int -> Int) 

since t1 is (Int -> Int) is maches expected types of t2

Therefore t3 inherits the result type of t2 when applied to t1, which is Int -> Int

1. f is type Int
2. \f:Int -> Int.\x:Int.f x, takes int ->
3.