Typed Lambda Calculus

Rules

• Integers are Church encoded (0, pred, succ)
• Abstraction is introduced by lam. Introduces a new variable.
• Abstraction is removed via app. Applies a value to a lambda abstraction.
• All variables are renamed uniquely

Typed Lambda Calculus

                                
id := (λa. a)
self apply := (λa. a a)
0 := (λf.a. a)
1 := (λf.a. f a)
2 := (λf.a. f  (f a))
...
true := (λa.b. a)
false := (λa.b. b)
pair := (λa.b.f. f (x y))
first := (λp. p (λa.b. a)) -- pair a b true
second := (λp. p (λa.b. b)) -- pair a b false
... etc
                                
                            

Typed Lambda Calculus

What about addition?

Could we use recursion?

The rules mean we can't use named recursion.

What about self application?

Y Combinator

More than Mohan's favorite news site

                                
fix := λf(.x. f (x x) (λx. f (x x)))
                                
                            

                                
fix :: (a -> a) -> a
fix f = let
    dupe fx = fx (dupe fx)
    in fx f
                                
                            

Y Combinator

Fixed Points

An input x where f(x)=x. Not all functions have them, some may have more than one.

-- All n <= 1 are fixed points
factorial :: Int -> Int
factorial = fix (\rec n -> if n <= 1 then 1 else n * rec (n-1))
                        
                        

Y Combinator

Defining Addition on Church numerals

fix (λf. (x,n). ->
        if isZero x
        then n
        else f (pred x, succ n)
    )
                        
                        

A Working Example

class LambdaCalc repr where
  zero :: repr Int
  pred :: repr Int -> repr Int
  succ :: repr Int -> repr Int

  lam :: forall a b. (repr a -> repr b) -> repr (a -> b)
  app :: forall a b. repr (a -> b) -> repr a -> repr b
  fix :: forall a. (repr a -> repr a) -> repr a

newtype Eval a = Eval a
unwrap :: forall a. Eval a -> a
unwrap (Eval a) = a


instance lambdaEval :: LambdaCalc Eval where
  zero = Eval 0
  pred (Eval 0) = Eval 0
  pred (Eval n) = Eval (n - 1)
  succ (Eval n) = Eval (n + 1)

  lam f = Eval $ unwrap <<< f <<< Eval
  app (Eval f) = \(Eval a) -> Eval (f a)
  fix f = Eval $ dupe (unwrap <<< f <<< Eval)
    where dupe fx = fx (dupe fx)

eval :: forall a. Show a => Eval a -> String
eval = show <<< unwrap