5. Type Safety: Progress and Preservation Theorems

Type Safety: Progress and Preservation Theorems

Type safety is a property of programming languages and type systems that ensures certain guarantees about the behavior of programs.

Two key theorems in type safety are the Progress theorem and the Preservation theorem.

The Progress theorem states that well-typed programs will never get stuck during evaluation.

This means that if a program can take a step of evaluation, it will do so.

Formally, if a term t is well-typed, then either t is a value or there exists another term t' such that t can take a step of evaluation to t'.

The Preservation theorem states that well-typed programs preserve their types under evaluation.

This means that if a program starts with a certain type, then after one step of evaluation, it will still have the same type.

Formally, if a term t has type T and t takes a step of evaluation to t', then t' also has type T.

Lab Activity: Implementing Type Safety Theorems

Let's implement a basic interpreter for a lambda calculus language in Python and verify the type safety properties using Progress and Preservation theorems.

class Term:
    def __init__(self, term, term_type):
        self.term = term
        self.term_type = term_type

def eval(term):
    # Evaluation logic
    pass

def type_check(term):
    # Type checking logic
    pass

def main():
    term = Term("λx: Bool. x", "Bool")
    try:
        result_type = type_check(term)
        print("Type:", result_type)
        result = eval(term)
        print("Result:", result)
    except Exception as e:
        print("Error:", e)

if __name__ == "__main__":
    main()
  

In the lab activity, we define a `Term` class to represent lambda expressions along with their types.

We implement functions for type checking (`type_check`) and evaluation (`eval`).

We then test the implementation with a sample lambda expression and observe the type and evaluation result.