Types

Types

 

“A type system is a tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute”

 

only can involve checking decidable properties of a program

  • e.g. can't detect divide by zero errors statically

 

Type systems restrict the set of sentences which are permitted over the language, in order to achieve the required safety properties

  • i.e. it rejects some valid programs

 

Untyped languages could be “safe” by performing certain checks at runtime

  • these hamper efficiency, and hence few untyped languages are “safe”

 

Trapped errors: those which can be handled gracefully

Untrapped errors: those which cause unpredictable crashes

 

Type soundness theorems: any well-typed program cannot produce run time errors of some specified kind

  • proofs can only occur after the syntax and operational semantics have been formally specified

 

Typing judgements:

Γ |- M : τ

 

Type checking problem: given Γ, M and τ is Γ |- M : τ derivable in the type system?

 

Typeability problem: given Γ and M is there any τ such that Γ |- M : τ derivable in the type system?

  • requires a type inference algorithm

 

polymorphism: forms

  • overloading, 'ad hoc polymorphism', e.g. + used for integers and floats

  • subsumption: if τ1 <: τ2 any M1 : τ1 can be used as M2 : τ2 safely

  • parametric polymorphism (or “generics”)

    • the same expression belongs to a family of structurally related types

 

Type variables:

  • variables for which types can be substituted

  • used to formalise

length : ∀τ (τ list → int)

 

Type scheme

  • e.g. ∀τ (τ list → int)

 

 

Mini-ML Types

τ ::= α type variable

| bool boolean type

| τ → τ function type

| τ list list type

 

where α ranges over a fixed, countably infinite set TyVar

 

Mini-ML Type schemes

σ ::= ∀ A (τ)

 

where A ranges over finite subsets of TyVar

 

for A = {α1 , ... , αn}, ∀ A (τ) is written

∀ α1 , ... , αn (τ)

 

NB

  • one can identify the type τ with the type scheme ∀ {} (τ)

    • this permits us to regard a set of types as a subset of the set of type schemes

  • bound type variables

    • type variable α which occurs in τ

    • αA

  • free type variables

    • type variable α which occurs in τ

    • αA

  • a type scheme is closed if it contains no free type variables

  • type schemes are identified up to α-conversion, therein are an equivalence class

  • ftv(∀ A (τ)) denotes the set of free type variables in τ

  • type schemes are not types!

 

Generalisation

  • a type scheme σ = α1 , ... , αn (τ') generalises type τ if, for some type variables αi and some types τi, i = 1 ... n

τ = τ'[τ1/α1 , ... , τn/αn]

  •  

    • i.e. if for some valid substitution of types for type variables we can derive τ from τ'

  • we write σ > τ

  • type τ specialises if σ > τ

  • NB

∀ α1 (α1 → α2) >/ α list → bool, as α2 is free and cannot be substituted for

 

M ::= x variable

| true

| false

| if M then M else M

| λx(M) function abstraction

| M M function applications

| let x = M in M

| nil nil list

| M :: M list cons

| case M of nil => M | x::x => M case expression

 

Mini-ML typing judgement

Γ |- M : τ

where Γ is a finite function from variables to type schemes

e.g. Γ {x1 : σ1 , ... , xn : σn}

M is an Mini-ML expression

τ is a Mini-ML type





NB

  • Γ, x : τ approximates Γ, x : ∀ {} (τ)

 

Principal type schemes for closed expressions

  • a closed type scheme ∀ A (τ) is the principal type scheme of a closed mini-ml expression M if

|- M : ∀ A (τ)

for any other closed type scheme ∀ A' (τ') if

|- M : ∀ A' (τ')

then ∀ A (τ) > τ'

Type substitutions

  • a type substitution S is

    • a totally defined function from type variables

    • S(α) = α for all but finitely many α

  • define the domain of SSub as

      dom(S) = {αTyVar | S(α) != α}

  • applying the substitution

    • to a type

        dom(S) = {α1 , ... , αn}

        S(αi) = τi

        S τ = τ[τ1/α1 , ... , τn/αn]

    • to a type scheme

      • S σ is the substitution of S(αi) for each free occurrence of αi in σ

 

Type unification

  • mgu τ1 τ2 returns either

    • SSub such that

      • S(τ1) = S(τ2)

      • ∀ S' . S'(τ1) = S'(τ2) => S' = T S

          where TSub

    • Fail iff τ1 and τ1 are not unifiable

 

Principle type schemes for expressions

  • the solution to the typing problem Γ |- M : ? is a pair (S, σ) s.t.

    • S Γ |- M : σ

      where

        S Γ = {x1 : S σ1 , ... xn : S σn}

  • a solution is principle if for any other (S', σ')

      TSub

    • T S = S'

    • T(σ) > σ' where σ > σ' means

      • σ' = ∀ A' (τ')

      • A'ftv(σ) ] {}

      • σ > τ'

 

NB

  • Γ |- M : σ => ∀ SSub . S Γ |- M : S σ

  • Γ |- M : σ /\ σ > σ' => Γ |- M : σ'

 

Principle typing algorithm

  • .....

  • come back to this

 

Polymorphic reference types

τ ::= ...

| unit

| τ ref

 

M ::= ...

| ()

| ref M

| !M

| M := M

 

 

  • typing rules can combine to create unsound type systems, e.g.

    •  
      •  

          (!r) () 3

        • let u = (r := λx' . ref !x' ) in 2

      • let r = ref λx . x in 1

    • we have

      •  

          the r on line 2 is typed as this, which is what allows it to use the let rule in typing

        • ref λx . x : ∀α . ((α → α) ref) = σ

        r : ∀α . ((α → α) ref) |- λx' . ref !x' : ∀α' . (α' ref → α' ref )

        σ > ( α' ref → α' ref ) ref

        σ > (unit → unit) ref

    • we can see that this will fail as when r is dereferenced it will have type ( α' ref → α' ref ) ref not type (α → α) ref, and it will attempt to do !()

  • Midi-ML transitions, includes

    •  

        V ::= x | λx.M | () | true | false | nil | V::V

    • <!x, s> → <s(x), s> if

    • <!V, s> → fail if V is not a variable

    • <if V then M1 else M2, s> → fail if V{true, false}

  • restoring type soundness

 

 

 

 

 

 

 

 

  •  

    • type soundness is defined as

      •  

          |- M : σ

          <M, {}> → ... → fail

        • for any closed Midi-ML expression M, if there is a type scheme such that σ

        is provable using the type system then there is no sequence of transitions which lead to a FAIL, i.e. there is no sequence such that

    • proving the type soundness is hard and is omitted

 

  •  

    • this new condition on the let rule prevents the earlier problem as

      •  

          due to the side condition

        • ref λx . x : ∀{} . ((α → α) ref) = σ

        r : (α → α) ref |- λx' . ref !x' : ∀α' . (α' ref → α' ref )

 

  •  
    •  
      •  

          σ > ( α' ref → α' ref ) ref

          σ > (unit → unit) ref

        • but this time we can't have both of

        since α is not universally quantified so the two types cannot both specialise σ

 

Polymorphic lambda calculus

  • also known as “second order typed lambda calculus”

  • there are some things we want to be able to type but can't yet, e.g.

    •  

      • this is not typeable as in the fn rule a trivial type scheme is assigned to x

      • something like (λx . x) would work fine

      • this is the fixed point combinator

      • can cause non-termination, but still it shouldn't cause a fail

      • λf . (f true) :: (f nil)

      λf .f f

  • polymorphic types are defined by combining monomorphic types and monomorphic type schemes

      π ::= α | bool | π → π | π list | ∀ α . ( π )

  • in order to make use of the →'s and ∀'s in polymorphic types it is necessary to replace the var axiom with


  • we can now type the previous problem expressions

------------------------------------- (id) ------------------------------------ (id)

f : ∀ α1 (α1) |- f : ∀ α1 (α1) f : ∀ α1 (α1) |- f : ∀ α1 (α1)

------------------------------------- (spec {1}) ----------------------------------- (spec {2})

f : ∀ α1 (α1) |- f : α2 → α2 f : ∀ α1 (α1) |- f : α2

--------------------------------------------------------------------- (app)

f : ∀ α1 (α1) |- f f : α2

-------------------------------------- (gen)

f : ∀ α1 (α1) |- f f : ∀ α2 (α2)

--------------------------------------------- (fn)

{} |- λf .f f : ∀ α1 (α1) → ∀ α2 (α2)

  •  
    •  

      • the first spec substitutes α2 → α2 for α1

      • the second spec substitutes α2 for α1

    • but note this is no longer syntax directed

  • in fact, the type checking and typeability problems are equivalent and undecidable

    • the gen and spec rules can be applied in many places

 

  • the polymorphic lambda calculus type system

    • if the language is explicitly typed then the type checking problem becomes trivial

        τ ::= α

        | τ → τ

        | ∀ α ( τ )

 

  •  
    •  

        M ::= x variable

        | λ x:τ . ( M ) function abstraction

        | M M function application

        | Λ α (M) type generalisation

        | M τ type specialisation

 

  •  

    • Λ α (M) is notation for the function F such that F( τ ) = M[τ/α]

      • i.e. it maps types to expressions

      • this is a beta reduction (meta)

        • similar to the normal beta reduction (λ x:τ . ( M1 )) M2 → M1 [M2/x]

    • it is often common to write specialisation (M τ ) as M τ

  • free type variables are defined by

    •  

        ftv(α) = {α}

        ftv(τ1 → τ2) = ftv(τ1) u ftv(τ2)

        ftv(∀ α ( τ )) = ftv(τ) – {α}

    • NB since types can occur in expressions we must also include

        ftv(x) = {}

        ftv(λ x:τ . ( M )) = ftv(τ) u ftv(M)

        ftv(M1 M2) = ftv(M1) u ftv(M1)

        ftv(Λ α (M) ) = ftv(M) – {α}

        ftv(M τ) = ftv(M) u ftv(τ)

  • free variables

    • as you would expect; occurrences of x in M become bound in λ x:τ . ( M )

  • substitutions

    • τ[ τ' / α ] denotes the type resulting from substituting all free occurrences of α in τ with τ'

    • M[ M' / x ] denotes the expression resulting from substituting all free occurrences of x in M with M'

    • M[ τ / α ] denotes the expression resulting from substituting all free occurrences of α in M with τ

  • the PLC type system:

 

 

 

 

 

 

 

 

 

 

 

 

  •  

    • NB, for proofs with gen to work you may need to rename types/type variables (by alpha equivalence), but since types are considered equivalent up to alpha conversion then the type without the changed names is still a valid type, even though you can't do the proof on it

  • PLC binding

      ∀ α ( _ ) α binds in _

      λ x:τ . ( _ ) x binds in _

      Λ α ( _ ) α binds in _

  • decidability of the PLC typeability and type checking problems

    • theorem

      • for each Γ |- M : ?

        • there is at most one τ such that Γ |- M : τ

          • this can be proved by induction on the structure of expressions

        • there is an algorithm which (for each Γ, M) either returns τ or FAILs otherwise

    • corollary

      • the PLC type checking problem is decidable

        • we can check if Γ |- M : τ by doing

            type(Γ, M) == τ

    • type

        type(Γ, Λ α (M)) := let τ = type(Γ, M) in ∀ α . (τ)

        type(Γ, M τ2 ) := let τ = type(Γ, M) in

        case τ of ∀ α . (τ1) → τ1[τ2 / α]

        | _ → FAIL

        ...

  • type associativity

    • α1 → α2 → α3 = α1 → (α2 → α3)

  • datatypes in PLC

    • defining a datatype representation includes

      • defining a suitable PLC type for the data

      • defining some PLC expression for the various operations associated with the data

      • demonstrating that these expressions have both the correct typings and the expected computational behaviour

    • beta reductions

      • M beta reduces to M' in one step M → M' means that

        • M' can be obtained from M by replacing a subexpression of M which is a redex by its corresponding reduct

      • in PLC redexes appear in the following expressions

        • λ x:τ . ( M )

          • in this case x is the redex

        • Λ α (M)

          • in this case α is the redex

      • in PLC reducts appear in the following expressions

        • (λ x:τ . ( M1 )) M2

          • M2 is the reduct

        • (Λ α (M)) τ

          • τ is the reduct

      • M →* M' indicates a chain ofbeta reductions

      • M is in beta normal form if it contains no redexes

      • properties of beta reduction on typeable expressions: given Γ |- M : τ

        • subject reduction

          • if M → M' then Γ |- M' : τ is also a provable typing

        • Church Rosser property

          • if M →* M1 and M →* M2 then there is a M' such that M1 →* M' and M2→* M'

        • strong normalisation property

          • there is no infinite chain M → M1 → M2 → ...

 

  •  
    •  

      • beta conversion

        •  

            M – . – ... – . – M'

          • M = β M' holds if there is a finite chain

          where each – is either ← or →

        • by Church Rosser and strong normalisation

          •  

              M →* N *← M'

            • M = β M' iff there is some Beta normal from N such that

    • non-termination can be represented as

      •  

          Ω := (λ f:α . (f f)) (λ f:α . (f f))

      • this has an infinite chain of beta reductions

      • PLC can be regarded a functional programming language where we reduce typeable expressions to beta normal form

        • since we don't have non-termination then the language is not Turing powerful

    • booleans

      •  
        •  

            if τ M1 M2 M3

          • NB, this is used as

          where τ is the common type of M2 and M3

        • bool = ∀ α . (α → (α → α))

        True = Λ α . (λ x1:α, x2:α . (x1))

        False = Λ α . (λ x1:α, x2:α . (x2))

        if = Λ α (λ b:bool, x1:α, x2:α . ( (b α) x1 x2 ))

      • True and False are the only closed beta normal forms in PLC of type bool, but it is beyond the scope of the course to prove it

    • lists

      •  

          Nil : ∀α . (α list)

          Λ α' (λ x':α', f:α→α'→α' . x') : α list

        •  

            (l α') x' f) : α'

          • Λ α' . (λ x':α', f:α→α'→α' . (f x ((l α') x' f))) : α list

          Cons : ∀α . (α → α list → α list)

        • α list = ∀α' (α' → (α' → α' → α') → α')

        Nil = Λ α, α' (λ x':α', f:α→α'→α' . x')

        Cons = Λ α . (λ x:α, l:α list . ( Λ α' . (λ x':α', f:α→α'→α' . (f x ((l α') x' f)))))

      • iteratively defined functions on (finite) lists

        • this is the “expected computational behaviour” which is required

            λ x':α' , f : α → α' → α' . (listIter x' f l) : α' → (α → α' → α') → α'

            is the algorithmic essence of l: α list

        • A* is a finite list of elements of the set A

        • given

          • a set A'

          • an element

          • a function f: A → A' → A'

        • we can define

            listIter x' f = ε g . (g Nil = x') /\ (g x::l = f x (g l))

        • i.e. listIter defines the unique function g: A*→A' such that

            g Nil = x'

            g x::l = f x (g l)

 

  •  
    •  
      •  

        • e.g.

          •  
            •  

                listIter 0 + := g

                g Nil = 0

                g (x::l) = + x (g l)

              • where

            • A' = int

            x' = 0

            + : A → int → int

            sum = listIter 0 +

      • in PLC we can define a function iter such that

        •  

            |- iter : ∀α , α' . (α' → (α → α' → α') → α list → α')

          • iter = Λ α, α' . (λ x':α', f:α → α' → α' , l:α list . (l α' x' f) )

        • using the definitions of Nil and Cons we can demonstrate that

            iter α α' x' f (Nil α) = β x'

            iter α α' x' f (Cons α x l) = β f x (iter α α' x' f l)

        • hence this iter satisfies the relevant requirements above

    • algebraic data types

      • these are data types which can be built up using sums and products of previously defined datatypes

      • all algorithmic types can be represented in PLC

      • lists, booleans and the following types are all algorithmic