This is a scratchpad.


  Y f  ≡αβη  f(Y f)

  Y not ≡αβη not(Y not)


  1    :: Int
  True :: Bool

Q: what's the type of not?

A: not :: Bool ⇒ Bool


   not True   <- this is valid because not :: Bool ⇒ Bool,
                                   and True :: Bool

  when you write s t
       s needs to have function type

  similarly to when you write f(x) in your favourite programming language,
       f needs to be a function


  (λx. x) 5 ↦β 5
  (λx. x) "hello world!" ↦β "hello world!"

  ^ (λx. x) is a *polymorphic* function,
            it can accept inputs of different type,
            so long as you return the same type you put in.

    (λx. x) :: α ⇒ α

We encode multi-argument function as nested lambdas:

   (λx. λy. x+y+1) 3 4 ↦β* 3+4+1

 Function application associates to the left for this reason

 For the same reason, *type arrows* need to associate to the right

   (λx. λy. x+y+1) :: Int ⇒ (Int ⇒ Int)
                    = Int ⇒ Int ⇒ Int


 [x ← Int] ⊢ (λy. y) x :: Int   <- typing judgement

 ^ In a context where x is an Int,
    (λy. y) x   has the type Int

  (λx. x) :: α ⇒ α


  _____________________ Var
  Γ[x ← Int] ⊢ x :: Int
 _________________________ Abs
  Γ ⊢ (λx. x) :: Int ⇒ Int


  (α ⇒ α)[α := Int] = (Int ⇒ Int)

  (α ⇒ β)[α := β, β := α]  = (β ⇒ α)  --- choice of type variable names doesn't matter
                                          up to alpha-equivalence

  3+4  reduces to 5,  luckily these terms both have type Int


 (λx. x x) (λx. x x)  <-- diverging term

 λf. ((λx. f (x x)) (λx. f (x x)))  <-- Y combinator


  ^ both of these involve *self-application*
        x x
    it turns out that all lambda-terms that have infinite computations
    involve self-application

    Self-application is not allow in our type system

        suppose x :: τ
               x :: τ ⇒ τ  x :: τ <-- this is impossible because τ ⇒ τ and τ are different
               ___________________
        Then   x x :: ??