Go backward to The Untyped lambda-Calculus Go up to Top Go forward to Basic and Structured Types

The Typed lambda-Calculus

• Extension of Untyped lambda-Calculus
  • Every variable must be explicitly typed when introduced as typed variable
  • Result types can be deduced from function body.
• Examples
  • value succ = fun(x:Int) x+1
  • value twice = fun(f: Int -> Int) fun(y:Int) f(f(y))
• Type declarations:
  • type IntPair = Int x Int
  • type IntFun = Int -> Int
• Type annotations/assertions:
  • (3, 4): IntPair
  • value intPair: IntPair = (3, 4)
• Local variables
  • let a = 3 in a+1
  • let a: Int = 3 in a+1