2015-03-17
Code Generation (Ch. 5-6)

Chapter 6: Intermediate-Code Generation

type (recursive definition)
  - basic types: boolean, char, integer, float, void
  - type name (type)
  - array (type, int)
  - record ((string, type)*)
  - function (type, type)

"structurally-equivalent" types
  - same basic type
  - same constructor applied to structurally-equivalent types
  - one is a type name that denotes the other

example: calculating the width of a field (Fig. 6.15)

Decaf types
  - type ("void")
  - type ("int")
  - type ("boolean")
  - array (type, int)
  - function ([type], type)
  - "==" operator for equivalence

type checking
  - type system: set of type rules
    - a system is "sound" if no dynamic checking is needed
    - languages with sound type systems are "strongly typed"
  - type checking
    - assign a type to every program component
    - verify that these types are valid according to the type system
  - static vs. dynamic type checking
    - static: done at compile time; can guarantee safety for all executions
      - overhead during compilation
    - dynamic: done at runtime; allows more flexible mixing of types
      - overhead at runtime
      - currently popular: "duck" typing
  - type synthesis vs. type inference
    - synthesis: determining the type of an expression from declared types
    - inference: determining the type of an expression from its use
      - allows for strong typing in the absence of typed declarations
  - type conversion - implicit vs. explicit and narrowing vs. widening
    - implicit: performed automatically by the compiler ("coercions")
    - explicit: specified by the programmer ("casts")
    - widening: preserves information
    - narrowing: may lose information
    - examples in Fig. 6.25
    - no need for widening or narrowing in Decaf
  - overloading
    - symbols with different meanings/types depending on context
    - can often be resolved by examining arguments
  - polymorphism: supporting multiple types
    - type inference: create type variables α, β, γ, etc.
    - substitution: mapping from type variable to type expressions
      - S(t) is an "instance" of t
      - e.g., list<int> is an instance of list<α>
    - "unify" variables and concrete type expressions using substitutions
    - unification algorithm (Fig. 6.32)

type inference example (Alg. 6.16 and Figs. 6.28, 6.29, 6.30)

    null : ∀t. [t] → bool
      tl : ∀t. [t] → [t]

  1)           length : α → β
  2)                x : α
  3)               if : bool × γ × γ → γ       β = γ
  4)             null : [δ] → bool
  5)          null(x) : bool                   α = [δ]
  6)                0 : int                    γ = int, β = int
  7)                + : int × int → int
  8)               tl : [ε] → [ε]
  9)            tl(x) : [ε]                    α = [ε]
  10)   length(tl(x)) : β                      β = int
  11)               1 : int
  12) length(tl(x))+1 : int
  13)        if (...) : int

    δ and ε remain unbound; thus the final type requires a quantifier:
       length : ∀t. [t] → int