Types in Computer Science

  • powerful frameworks: Hoare logic, algebraic specification lagnauges, modal logics and denotational semantics
  • modest power: model checkers, run-time monitoring, type systems(most popular, best established lightweight formal method)

Definition of type system:

  • tractable syntatic method
    • typecheckers (compilers + linkers) should be able to do their job automatically, with no manual intervention (though require type annotations)
  • for proving the absence of certain program behaviors
    • being static, type systems are conservative, they can categorically prove the absence of some bad program behaviors
  • by classifying phrases according to the kinds of values they compute
    • type system can be regarded as a static approximation to the run-time behaviors of the terms in a program.

Comments:

  • type system as tool for reasoning about programs.

Branches of type systems

  • more practical branch concerned with programming languages (focus of book)
    • sacrifice termination propterties for the sake of features like recursive function definitions
  • abstract focused on connections between various “pure typed lambda-calculi” and varities of logic, via the Curry-Howard correspondence
    • every well-typed computation is guranteed to terminate

What type systems are good for

  • Detecting Errors
    • early detection of programming errors
  • Abstraction
    • module languages: types show up in the interfaces of modules (and related structures, e.g. classes)
  • Documentation
    • Type useful when reading programs
  • Language Safety
    • protects its own abstractions
    • untrapped errors
    • portabilities
  • Efficiency
    • High performance due to information collected by typechecker
  • Futher Applications
    • Computer & Network Security
    • Program analysis tools (other than compilers)
    • Alias Analysis
    • Exception Analysis
    • Automated Theorem Proving
    • Databases: e.g. new languages for querying and manipulating XML
    • Computational Linguistics

Type System and Language Design

  • Retrofitting type system onto a language not designed with typechecking can be tricky
    • offer features/encourage programming idioms that make typehchecking difficult/infeasible.
    • concrete syntax of typed languages more complicated than untyped languages.