About these lecture notes
                                   Simply Typed λ-Calculus
                                Akim Demaille akim@lrde.epita.fr                                Many of these slides are largely inspired from Andrew D. Ker’s lecture notes
                                                                                                [Ker, 2005a, Ker, 2005b]. Some slides are even straightforward copies.
                          EPITA — École Pour l’Informatique et les Techniques Avancées
                                            June 14, 2016
                                                                                                        A. Demaille                     Simply Typed λ-Calculus          2 / 46
            Simply Typed λ-Calculus                                                            Types
                                                                                                1  Types
             1  Types                                                                                Untyped λ-calculus
                                                                                                     Paradoxes
             2  λ→: Type Assignments                                                                 Church vs. Curry
                                                                                                2   →
                                                                                                   λ : Type Assignments
                     A. Demaille                     Simply Typed λ-Calculus          3 / 46            A. Demaille                     Simply Typed λ-Calculus          4 / 46
            Types                                                                              Types
                                                                                               Types first appeared with
                                                                                                    Curry (1934) for Combinatory Logic
                                                                                                    Church (1940)
                                                                                               Types are syntactic objects assigned to terms:
                                                                                                                         M:A       Mhastype A
                                                                                               For instance:
                                                                                                                                I : A → A
                 Alonzo Church (1903–1995)               Haskell Curry (1900–1982)
                     A. Demaille                     Simply Typed λ-Calculus          5 / 46           A. Demaille                     Simply Typed λ-Calculus          6 / 46
            Untyped λ-calculus                                                                 λ-terms
             1  Types
                  Untyped λ-calculus                                                           Λ, set of λ-terms
                  Paradoxes
                  Church vs. Curry                                                                             x ∈ V      M∈Λ N∈Λ                M∈Λ x∈V
                 →                                                                                       x ∈ Λ              (MN)∈Λ            (λx · M) ∈ Λ
             2  λ : Type Assignments
                     A. Demaille                     Simply Typed λ-Calculus          7 / 46           A. Demaille                     Simply Typed λ-Calculus          8 / 46
            λβ                                                                                 Properties of λβ
             The λβ Formal System
                                           M=N         M=N N=L                                  β-reduction is Church-Rosser.
                              M=M N=M                       M=L                                 Any term has (at most) a unique NF.
                               M=M′ N=N′                   M=N                                  β-reduction is not normalizing.
                                  MN=M′N′             λx · M = λx ·N
                                                                                                Some terms have no NF (Ω).
                                        (λx · M)N = [N/x]M
                     A. Demaille                     Simply Typed λ-Calculus          9 / 46            A. Demaille                     Simply Typed λ-Calculus         10 / 46
            Paradoxes                                                                          Self application
             1  Types
                  Untyped λ-calculus                                                            What is the computational meaning of λx · xx?
                  Paradoxes
                  Church vs. Curry                                                                   Stop considering anything can be applied to anything
                                                                                                     A function and its argument have different behaviors
             2  λ→: Type Assignments
                     A. Demaille                     Simply Typed λ-Calculus         11 / 46            A. Demaille                     Simply Typed λ-Calculus         12 / 46
            Church vs. Curry                                                                  Simple Types
             1  Types                                                                              A set of type variables
                  Untyped λ-calculus
                  Paradoxes                                                                        α,β,...
                  Church vs. Curry                                                                 A symbol → for functions
                                                                                                   α→α,α→(β→γ),(α→β)→γ,...
             2  λ→: Type Assignments                                                               Possibly constants for “primitive” types
                                                                                                   ι for integers, etc.
                    A. Demaille                     Simply Typed λ-Calculus         13 / 46           A. Demaille                     Simply Typed λ-Calculus         14 / 46
            Simple Types                                                                      Alonzo Style, or Haskell Way?
             By convention → is right-associative:
                                    α→β→γ=α→(β→γ)                                                  Church:                             Curry:
                                                                                                   Typed λ-calculus                    λ-calculus with Types
             This matches the right-associativity of λ:                                                        x : α                                x : α
                                                                                                          λxα·x : α → α                        λx · x : α → α
                                    λx · λy · M = λx · (λy · M)
                    A. Demaille                     Simply Typed λ-Calculus         15 / 46           A. Demaille                     Simply Typed λ-Calculus         16 / 46