Simply Typed Lambda Calculus

Untyped Lambda Calculus

Untyped Lambda Calculus - Recapitulation

We can boil down computation to a tiny calculus

All we need is:

Function Definition / Abstraction ($λ x . e$)
Function Application ($e \ e$)
Parameters / Variables ($x$)

Then we get:

Booleans
Numerals
Data Structures
Control Flow
…

Turing Completeness

If it can be computed, it can be computed in Lambda Calculus!

Example - $(λ p . λ q . p) \ a \ b$

\begin{align*} \onslide<1->{ & ( λ \color<3->{orange}{p} . & λ q . & \color<3->{orange}{p} & ) & & \color<3->{orange}{a} & & b & & \onslide<2->{ \text{Substitute $p \mapsto a $}} }
\onslide<4->{ & ( & λ \color<6->{blue}{q} . & \color<4->{orange}{a} & ) && & & \color<6->{blue}{b} & & \onslide<5->{ \text{Substitute $q \mapsto b $}} } \ \onslide<7->{ & ( & & \color<4->{orange}{a} & ) && & & & & } \end{align*}

Meaning

$λ p . λ q . p$: Is a function that returns a function ($λ q . p$)
$a , b$: Some variables (defined somewhere else)
$p$: Is a variable that is bound to the parameter with the same name

Build an Interpreter

Let’s build an interpreter

Deepen our intiution
Later move on to the Simply Typed Lambda Calculus
- Why do we need types?
- How does a type checker work?
- How does it restrict the programs we might write?
We’ll do Math Driven Development
- Look at the concepts in math first, then translate them to Haskell

Structure

\begin{align*} e ::= & & \text{Expressions:}
& \ x & \text{Variable} \ & \ λ x.e & \text{Abstraction} \ & \ e \ e & \text{Application} \end{align*}

$λ x.e$: Function Definition
$e \ e$: Function Application (Function Call)

Abstract Syntax Tree

Lambda Expression

$(λ x . x) \ y$

AST

digraph untyped_lambda_calculus_ast {
  App [label = "Application"];
  Lam [label = "Lambda"]
  Param [label = "Parameter: x"]
  VarX [label = "Variable: x"]
  VarY [label = "Variable: y"]

  App -> {Lam VarY}
  Lam -> {Param VarX}

}

Underneath

Meaning

Identity function $(λ x . x)$ is applied to a variable ($y$)

Interpreter - Syntax

module UntypedSyntax where

type Name = String

data Expr                    -- $e ::= \ \ \ \ \ \ \ \ \ \ \ \text{Expressions:}$
  = Var Name                 --       $x \ \ \  \ \ \ \ \ \ \ \ \text{Variable}$
  | Lambda Name              --       $\lambda x.e \ \ \  \ \ \ \ \text{Abstraction}$
           Expr
  | App Expr                 --       $e \ e \ \ \  \ \ \ \ \ \ \text{Application}$
        Expr
  deriving (Eq, Show)

Interpreter - Syntax - Examples

module UntypedSyntaxExamples where

import UntypedSyntax

-- $id \equiv \lambda x . x$
id :: Expr
id = Lambda "x" $ Var "x"

-- $true \equiv \lambda p . \lambda q . p$
true :: Expr
true = Lambda "p" (Lambda "q" (Var "p"))

-- $false \equiv \lambda p . \lambda q . q$
false :: Expr
false = Lambda "p" (Lambda "q" (Var "q"))

Interpreter - Syntax - Examples

-- $and \equiv \lambda p . \lambda q . p \ q \ p$
and :: Expr
and = Lambda "p" $ Lambda "q" $ App (App (Var "p") (Var "q")) (Var "p")

Natural Deduction

Notation

\begin{align*} \frac{}{Axiom} & \quad & \text{(A1)} \
\frac{Antecedent}{Conclusion} & \quad & \text{(A2)} \ \ \end{align*}

Meaning

Axiom: Rule without Precondition
Antecedent: Precondition - if it’s fulfilled this rule applies
Conclusion: What follows from this rule
A1, A2: Names for the rules

Proof: 2 is a Natural Number

Rules

\begin{align*} \frac{}{0 : \mathtt{Nat}} & \quad & \text{(A1)} \
\frac{n : \mathtt{Nat}}{\mathtt{succ}(n) : \mathtt{Nat}} & \quad & \text{(A2)} \ \ \end{align*}

\onslide<2->

Proof

\begin{equation*} \dfrac { \quad \dfrac { \quad \dfrac{} { 0 : Nat } \quad \text{(A1)} } { succ(0) : Nat } \quad \text{(A2)} } { succ(succ(0)) : Nat } \quad \text{(A2)} \end{equation*}

Underneath

\vspace{-0.5cm} \onslide<1->

Meaning

A1: $0$ is a natural number (by definition)
A2: The successor of a natural number is a natural number

\onslide<2->

$→$: Thus the successor of the successor of $0$ ($2$) must be a natural number

Evaluation Rules

Evaluation Rules - Call by Value - E-App1

\begin{align*} \frac{e_1 → e_1’}{e_1 e_2 → e_1’ e_2} & \quad & \text{E-App1} \
\end{align*}

Meaning

Under the condition that $e_1$ can be reduced further, do it.

Evaluation Rules - E-App1 - Example

\begin{equation*} \frac{e_1 → e_1’}{e_1 e_2 → e_1’ e_2} \end{equation*}

Example

\begin{align*} & \overbrace{\alert<2->{((λ x.x) \ (λ y.y))}}^e_1 \ e_2
\onslide<3->{→ & \alert<3->{(λ y.y)} \ z} \end{align*}

Evaluation Rules - Call by Value - E-App2

\begin{align*} \frac{e_2 → e_2’}{v_1 e_2 → v_1 e_2’} & \quad & \text{E-App2} \
\end{align*}

Meaning

Under the condition that $e_2$ can be reduced further and $v_1$ is a value, do it.
“Bare” Untyped Lambda Calculus:
- Only Lambdas (functions) are values.
- But you can add Ints, Booleans, etc. (“Enriched Untyped Lambda Calculus”)

Evaluation Rules - E-App2 - Example

\begin{align*} \frac{e_2 → e_2’}{v_1 e_2 → v_1 e_2’} & \quad & \text{E-App2} \
\end{align*}

\vspace{-0.5cm}

Example

\begin{align*} & \overbrace{(λ x.x)}^v_1 \ \overbrace{\alert<2->{((λ y.y) \ 42)}}^e_2
\onslide<3->{→ & (λ x.x) \ \alert<3->{42}} \end{align*}

\vspace{-0.5cm} \onslide<4->

Note

We evaluate the parameter before applying the function: Eager Evaluation!

Evaluation Rules - Call by Value - E-AppLam

\begin{align*} {(λ x . e) v → [x / v] e } & \quad & \text{E-AppLam} \
\end{align*}

Meaning

If a lambda (function) is applied to a value, substitute that value for it’s parameter.
“substitute” : replace it for every occurence in the lambda’s body

Evaluation Rules - E-AppLam -Example

\begin{align*} {(λ x . e) v → [x / v] e } & \quad & \text{E-AppLam} \
\end{align*}

Example

\begin{align*} & \overbrace{(\alert<2->{λ x.} λ y.\alert<2->{x})}^{λ x.e} \ \overbrace{\alert<2->{z}}^v
\onslide<3->{→ & λ y .\alert<3->{z}} \end{align*}

Interpreter - Evaluation

module UntypedEval where

import UntypedSyntax

eval :: Expr -> Expr
-- No rule for variables
eval variable@(Var _) = variable
-- No rule for lambdas
eval lambda@(Lambda _ _) = lambda

Interpreter - Evaluation

eval (App e1 e2)
--
-- $ \frac{e_1 \to e_1'}{e_1 e_2 \to e_1' e_2} \quad (E-App1) $
--
 =
  let e1' = eval e1
--
-- $ \frac{e_2 \to e_2'}{v_1 e_2 \to v_1 e_2'} \quad (E-App2) $
--
   in let e2' = eval e2
       in case e1'
                of
--
-- $ {(\lambda x . e) v \to [x / v] e } \quad (E-AppLam) $
--
            (Lambda x e1'_body) -> eval $ substitute x e2' e1'_body
            e1' -> App e1' e2'

Interpreter - Substitution

substitute :: Name -> Expr -> Expr -> Expr
--
-- If the Name matches: Substitute this Var by it's substitution
-- Otherwise: Leave it as is
--
substitute name substitution var@(Var varName)
  | name  == varName = substitution
  | otherwise = var
--
-- Recursively substitute in both parts of Applications
--
substitute name substitution (App term1 term2) =
  App (substitute name substitution term1) (substitute name substitution term2)

Interpreter - Substitution

--
-- Only substitute in Lambda's body, if the parameter doesn't
-- redefine the Name in it's scope
--
substitute name substitution lambda@(Lambda varName term) =
  if name == varName
    then lambda
    else Lambda varName (substitute name substitution term)

Tests

module UntypedEvalExamplesSpec where

import NaiveUntypedEval
import Prelude hiding (and)
import Test.Hspec
import UntypedSyntax
import UntypedSyntaxExamples

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  describe "eval" $
    it "should evaluate these terms"  $ do
--
-- $a \to a $
--
      eval (Var "a") `shouldBe` Var "a"

Tests

--
-- $true \equiv \lambda p . \lambda q . p$ 
--
-- $true \ a \ b \to a$
--
      eval (App (App true (Var "a")) (Var "b")) `shouldBe` Var "a"

--
-- $false \equiv \lambda p . \lambda q . q$
--
-- $and \equiv \lambda p . \lambda q . p \ q \ p$
--
-- $and \ true \ false \to false$
--
      eval (App (App and true) false) `shouldBe`
        Lambda "p" (Lambda "q" (Var "q"))

Simply Typed Lambda Calculus

Structure

\begin{align*} e ::= & & \text{Expressions:}
& \ x & \text{Variable} \ & \ λ x \alert{:τ}.e & \text{Abstraction} \ & \ e \ e & \text{Application} \end{align*}

$τ$

Type of the parameter $x$

Bool, Int, …

What’s a Type?

A Type is a set of values that an expression may return:

Bool: True, False
Int: $[-2²⁹ .. 2²⁹-1]$ (in Haskell, `Data.Int`)

Simple types don’t have parameters, no polymorphism:

Bool, Int: have no parameters $→$ simple types
Maybe a: takes a type parameter ($a$) $→$ not a simple type
a -> a: is polymorphic $→$ not a simple type

Type Safety = Progress + Preservation

Progress : If an expression is well typed then either it is a value, or it can be further evaluated by an available evaluation rule.

A well typed (typeable) program never gets “stuck”.

Preservation : If an expression $e$ has type $τ$, and is evaluated to $e’$, then $e’$ has type $τ$.

$e ≡ (λ x: Int.x) 1$ and $e’ ≡ 1$ have both the same type: Int

Not all meaningful Programs can be type checked

id :: a -> a
id a = a

It strongly depends on the type system if this is allowed or not.
In Simply Typed Lambda Calculus it’s not!
- No polymorphic types …

Evaluation

Evalution rules stay the same!

Type checking is done upfront

Typing Rules - Variables

\begin{align*} \frac{x:τ ∈ Γ}{Γ \vdash x:τ} & \quad & \text{T-Var} \
\end{align*}

Meaning

Γ

The Typing Environment, a list of $(Variable : Type)$ pairs (associations)

Think of a map: $Variable \mapsto Type$

Condition

If $(x, τ)$ is in the Typing Environment

Conclusion

$x$ has type $τ$

Typing Rules - Variables - Example

\begin{align*} \frac{x:τ ∈ Γ}{Γ \vdash x:τ} & \quad & \text{T-Var} \
\end{align*}

Example

\begin{align*} \underbrace{λ x:Int}_{Γ’ = Γ , x:Int}. \underbrace{λ y:Bool}_{Γ” = Γ’, y:Bool}.\underbrace{x}_{Γ” \vdash x:Int} \end{align*}

$λ x:Int$: Add $x:Int$ to the Typing Environment ($Γ$)
$x$: We know from the Typing Environment ($Γ”$) that $x$ has type $Int$

Typing Rules - Constants

\vspace{-0.5cm} \begin{align*} Γ \vdash n : \text{Int} & \quad & \text{T-Int} \
Γ \vdash \text{True} : \text{Bool} & \quad & \text{T-True} \ \ Γ \vdash \text{False} : \text{Bool} & \quad & \text{T-False} \ \ \end{align*}

\vspace{-1.5cm}

Meaning

True, False: literals / constants are of type Bool
$n$: number literals / constants are of Int

Why do we need $Γ$ here?

We handle Type Constructors like variables
Think: $Γ ≡ ∅ , True : Bool, False : Bool, 0 : Int, 1 : Int, …$

Typing Rules - Constants - Example

\begin{align*} Γ \vdash n : \text{Int} & \quad & \text{T-Int} \
Γ \vdash \text{True} : \text{Bool} & \quad & \text{T-True} \end{align*}

Example

\begin{align*} & Γ ≡ ∅ , \textcolor<2->{mLightGreen}{True : Bool}, False : Bool, 0 : Int, \textcolor<3->{mLightBrown}{1 : Int}, … \
& \textcolor<2->{mLightGreen}{True} \ & \textcolor<3->{mLightBrown}{1} \end{align*}

Typing Rules - Lambdas

\begin{align*} \frac{Γ, x : τ_1 \vdash e : τ_2}{Γ \vdash λ x:τ_1 . e : τ_1 → τ_2 } & \quad & \text{T-Lam} \
\end{align*}

Meaning

Condition: With $x : τ_1$ in the Typing Environment, $e$ has type τ_2
Conclusion: $λ x:τ_1 . e$ has type $τ_1 → τ_2$

Because $e$ has type τ_2 if $x$ has type τ_1

Typing Rules - Lambdas - Example

\begin{align*} \frac{Γ, x : τ_1 \vdash e : τ_2}{Γ \vdash λ x:τ_1 . e : τ_1 → τ_2 } & \quad & \text{T-Lam} \
\end{align*}

Example

\begin{align*} & λ x: \overbrace{Int}^τ_1 . \overbrace{x}^e & : & \onslide<1-2>{?} \onslide<3->{\overbrace{Int → Int}^{τ_1 → τ_2} } \
\onslide<2->{& \frac{Γ, x : \overbrace{Int}^τ_1 \vdash e : \overbrace{Int}^τ_2}{Γ \vdash λ x: \underbrace{Int}_{τ_1} . e : \underbrace{Int → Int}_{τ_1 → τ_2} }} \end{align*}

Typing Rules - Applications

\begin{align*} \frac{Γ \vdash e_1 : τ_1 → τ_2 \quad Γ \vdash e_2 : τ_1}{Γ \vdash e_1 e_2 : τ_2} & \quad & \text{T-App} \
\end{align*}

Meaning

Condition: If $e_1$ is a function of type $τ_1 → τ_2$ and $e_2$ has type $τ_2$
Conclusion: Then the type of $e_1 e_2$ (function application) is $τ_2$

id' :: Int -> Int
id' i = i

1 :: Int
(id' 1) :: Int

Typing Rules - Applications - Example

\begin{align*} \frac{Γ \vdash e_1 : τ_1 → τ_2 \quad Γ \vdash e_2 : τ_1}{Γ \vdash e_1 e_2 : τ_2} & \quad & \text{T-App} \
\end{align*}

Example

\begin{align*} & \overbrace{(λ x:Int. True)}^e_1 \overbrace{42}^e_2 & : & \onslide<1-2>{?} \onslide<3->{\overbrace{Bool}^τ_2} \
\onslide<2->{ & \frac{Γ \vdash \overbrace{(λ x:Int. True)}^e_1 : \overbrace{Int → Bool}^{τ_1 → τ_2} \quad Γ \vdash \overbrace{42}^e_2 : \overbrace{Int}^τ_1}{Γ \vdash \underbrace{(λ x:Int. True)}_{e_1} \underbrace{42}_{e_2} : \underbrace{Bool}_{τ_2}}} \end{align*}

Type Checker - Expressions

module TypedSyntax where

import qualified Data.Map.Strict as Map

type Name = String
type Error = String

data Expr                    -- $e ::= \quad \quad \quad \quad \quad \quad \quad \quad Expressions:$
  = IntValue Int             --     $[-2^{29} .. 2^{29}-1] \quad \quad \quad \quad \quad \text{Integer Literal}$
  | BoolValue Bool           --     $True \ | \ False \quad \quad \quad \quad \quad \quad \ \text{Boolean Literal}$
  | Var Name                 --     $x \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \ \text{Variable}$
  | App Expr                 --     $e \ e \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \ \text{Application}$
        Expr
  | Lambda Name              --     $\lambda x \mathbf{:\tau}.e \quad \quad \quad \quad \quad \quad \quad \quad \ \text{Abstraction}$
           Type
           Expr
  deriving (Eq, Show)

Type Checker - Types

type Environment = Map.Map Name Type

data Type                    -- $\tau ::= \quad \quad \quad \quad \quad \quad Types:$
  = TInt                     --     $Int \quad \quad \quad \quad \quad \quad \text{Integer}$
  | TBool                    --     $Bool \quad \quad \quad \quad \quad \ \text{Boolean}$
  | TArr Type                --     $\tau_1 \to \tau_2 \quad \quad \quad \ \ \text{Abstraction / Function}$
         Type
  deriving (Eq, Show)

Type Checker - Literals

module TypedCheck where

import Data.Either.Extra
import qualified Data.Map.Strict as Map

import TypedSyntax

check :: Environment -> Expr -> Either Error Type
--
-- $ \Gamma \vdash n : \text{Int}  \quad  \text{(T-Int)} $
--
check _ (IntValue _) = Right TInt
--
-- $ \Gamma \vdash \text{True} : \text{Bool}  \quad  \text{(T-True)} $
--
check _ (BoolValue True) = Right TBool
--
-- $ \Gamma \vdash \text{False} : \text{Bool}  \quad   \text{(T-False)} $
--
check _ (BoolValue False) = Right TBool

Type Checker - Lambda Abstraction

--
-- $ \frac{\Gamma, x : \tau_1 \vdash e : \tau_2}{\Gamma \vdash \lambda x:\tau_1 . e : \tau_1 \rightarrow \tau_2 }  \quad  \text{(T-Lam)} $
--
check env (Lambda x t1 e) = do
  t2 <- check (Map.insert x t1 env) e
  return $ TArr t1 t2

Type Checker - Application

--
-- $  \frac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1}{\Gamma \vdash e_1 e_2 : \tau_2}  \quad  \text{(T-App)} $
--
check env (App e1 e2) = do
  te1 <- check env e1
  case te1 of
    (TArr t1 t2) -> do
      te2 <- check env e2
      if t1 == te2
        then Right t2
        else Left $ "Expected " ++ (show t1) ++ " but got : " ++ (show te2)
    _ -> Left $ "Expected TArr but got : " ++ (show te1)

Type Checker - Variables

--
-- $  \frac{x:\tau \in \Gamma}{\Gamma \vdash x:\tau}  \quad  \text{(T-Var)} $
--
check env (Var x) = find env x

find :: Environment -> Name -> Either Name Type
find env name = maybeToEither "Var not found!" (Map.lookup name env)

Tests

module TypedCheckExamplesSpec where

import Test.Hspec
import TypedCheck
import TypedSyntax

import qualified Data.Map.Strict as Map

main :: IO ()
main = hspec spec

Tests

spec :: Spec
spec = do
  describe "check" $
    it "should type check these terms" $
--
-- $(\lambda x:Int . x) \ 42 :: Int $
--
     do
      check Map.empty (App (Lambda "x" TInt (Var "x")) (IntValue 5)) 
        `shouldBe` Right TInt

--
-- Does not type check: $(\lambda x:Bool . x) \ 42$
--
      check Map.empty (App (Lambda "x" TBool (Var "x")) (IntValue 5)) 
        `shouldBe` Left "Expected TBool but got : TInt"

Tests

--
-- Does not type check: $42 \ False$
--
      check Map.empty (App (IntValue 42) (BoolValue False)) `shouldBe`
        Left "Expected TArr but got : TInt"

End

Thanks

Hope you enjoyed this talk and learned something new.
Hope it wasn’t too much math and dusty formulas … :)

Books

Good Math

Image

Description

A Geek’s Guide to the Beauty of Numbers, Logic, and Computation

Easy to understand

Types and Programming Languages

Image

Description

Types systems explained by building interpreters / checkers and proving properties
Very “mathematical”, but very complete and self-contained

Write you a Haskell

Image

Description

Building a modern functional compiler from first principles.

Starts with the Lambda Calculus and goes all the way down to a full Haskell compiler
Available for free - Not finished, yet

Files

presentation_2.org

Latest commit

History

presentation_2.org

File metadata and controls

Simply Typed Lambda Calculus

Untyped Lambda Calculus

Untyped Lambda Calculus - Recapitulation

We can boil down computation to a tiny calculus

All we need is:

Then we get:

Turing Completeness

Example - $(λ p . λ q . p) \ a \ b$

Meaning

Build an Interpreter

Let’s build an interpreter

Structure

Abstract Syntax Tree

Lambda Expression

AST

Underneath

Meaning

Interpreter - Syntax

Interpreter - Syntax - Examples

Interpreter - Syntax - Examples

Natural Deduction

Notation

Meaning

Proof: 2 is a Natural Number

Rules

Proof

Underneath

Meaning

Evaluation Rules

Evaluation Rules - Call by Value - E-App1

Meaning

Evaluation Rules - E-App1 - Example

Example

Evaluation Rules - Call by Value - E-App2

Meaning

Evaluation Rules - E-App2 - Example

Example

Note

Evaluation Rules - Call by Value - E-AppLam

Meaning

Evaluation Rules - E-AppLam -Example

Example

Interpreter - Evaluation

Interpreter - Evaluation

Interpreter - Substitution

Interpreter - Substitution

Tests

Tests

Simply Typed Lambda Calculus

Structure

What’s a Type?

Type Safety = Progress + Preservation

**Progress** : If an expression is well typed then either it is a value, or it can be further evaluated by an available evaluation rule.

**Preservation** : If an expression $e$ has type $τ$, and is evaluated to $e’$, then $e’$ has type $τ$.

Not all meaningful Programs can be type checked

Evaluation

Evalution rules stay the same!

Typing Rules - Variables

Meaning

Typing Rules - Variables - Example

Example

Typing Rules - Constants

Meaning

Why do we need $Γ$ here?

Typing Rules - Constants - Example

Example

Typing Rules - Lambdas

Meaning

Typing Rules - Lambdas - Example

Example

Typing Rules - Applications

Meaning

Typing Rules - Applications - Example

Example

Progress : If an expression is well typed then either it is a value, or it can be further evaluated by an available evaluation rule.

Preservation : If an expression $e$ has type $τ$, and is evaluated to $e’$, then $e’$ has type $τ$.