2. Basic Concepts of Type Theory

Basic Concepts of Type Theory

In Type Theory, types are fundamental constructs that classify various entities in a formal system.

Each entity, known as a term, is assigned a type, indicating its nature or category.

Terms represent objects, values, or expressions within the system, while types categorize these terms based on their properties.

For example, in a simple type system, we might have types such as Bool, Nat, and λ, and corresponding terms like true, 42, and λx.x.

Judgments are statements or propositions about the relationship between terms and types, indicating whether a term belongs to a particular type.

In a type judgment, we use notation like term : type to express that a given term is of a specific type.

For instance, true : Bool indicates that the term true belongs to the type Bool.

Lab Activity: Simple Type Checking

Let's implement a basic type checker for a simple language with Boolean and Natural Number types.

def type_check(term):
    if term in ["true", "false"]:
        return "Bool"
    elif term.isdigit():
        return "Nat"
    else:
        raise ValueError("Unknown term")

def main():
    terms = ["true", "42", "add", "hello"]
    for term in terms:
        try:
            result = type_check(term)
            print("Term:", term, "Type:", result)
        except ValueError as e:
            print("Error:", e)

if __name__ == "__main__":
    main()
  

The `type_check` function takes a term as input and returns its type if it belongs to a known type category, otherwise raises an error.

We define the type categories based on the known terms such as Boolean literals and natural numbers.

You can then test the type checker with various terms and observe the judgments made about their types.