Types and Type System

Type

What is a type? Also see Data Type.

Below is information summarized from the following sources (recommended by Teacher):

• Type Systems
• In Search of Types
• Against a universal definition of ‘type’

Summarized in three categorizations:

1. A type can be defined as a collection of values, such as integers, characters, strings, programs, trees, sounds, images, videos, etc
2. a type is as an interpretation of sequences of bits.
   1. Ex: 1001 mean the number 9 when interpreted as an unsigned, -7 when interpreted as a two’s-complement integer. You can also interpret the number as ASCII the letter
3. A type is a computable property of programs that guarantees some property about their execution
   1. Ex: if a compiler determines that some expression has the type Int, then the expression always produces integer values when it is evaluated

Type System

A type system is a collection of Inference Rule that define a typing relation. A typing relation $T$ is a set of triples $⟨\Gamma ,E,\tau ⟩$, where

• $\Gamma$ is a typing context in the terminology of type systems and corresponds to a symbol table in our compiler
  • In the compiler, a symbol table maps each identifier to its meaning, a declaration of that identifier in the program
• $E$ is called a term in the terminology of type systems and corresponds to a subtree of the Parse Tree in our compiler implementation
• $\tau$ is a type

Type Soundness

Wow, see Soundness, it’s exactly the same idea.

We say that a type system is sound if whenever the expression tree $E$ has type $\tau$ in the typing relation, then during the execution of a program, the expression $E$ evaluates to a value of the type $\tau$.

For the LACS Language, we have these rules