Theta Type Checker

The Theta TypeChecker ensures that all expressions and statements in the abstract syntax tree (AST) conform to the language’s type rules. It validates the types of variables, function parameters, return values, and operations to prevent type mismatches, thereby guaranteeing the correctness of code before generating WebAssembly.

This document details the architecture and flow of the TypeChecker, providing insights into how types are checked, verified, and enforced throughout the AST.

Table of Contents

  1. Overview
  2. Core Components
  3. Detailed Type Checking Process
  4. Design Considerations
  5. Example Workflow

Overview

The Theta TypeChecker traverses the abstract syntax tree (AST) generated by the parser and verifies that each node adheres to the language’s type constraints. It tracks variable declarations, function signatures, and type assignments to ensure type correctness throughout the program.

Goals:

  • Enforce Type Consistency: Ensure that types in expressions, statements, and operations match expected values.
  • Detect Type Errors: Catch issues such as assigning incompatible types or invoking functions with incorrect parameter types.

Core Components

Type Validation

The heart of the TypeChecker is the checkNode() function, which verifies the type of each AST node. Depending on the node’s type, the TypeChecker applies specific validation rules.

Key Responsibilities:

  • Expression Checking: Validate that binary and unary operations use compatible types (e.g., integers with integers).
  • Literal Checking: Ensure that literals (numbers, strings, booleans) are correctly typed.
  • Function Return Types: Check that the return type of a function matches its declaration.

Scope Management

The TypeChecker manages scopes to keep track of variable and function declarations. Each new scope (such as within a function or block) introduces a new context for variable declarations.

  • Enter Scope: When processing a new block or function, the TypeChecker enters a new scope to manage local variables.
  • Exit Scope: Upon exiting a block, the scope is discarded, ensuring that variables are not accessible outside their defined range.

Detailed Type Checking Process

Checking Nodes

Each AST node represents a different construct in the language (e.g., a function, a variable, an operation). The checkNode() function identifies the type of the node and verifies its correctness.

  • Literal Nodes: Directly assign a type to the node (e.g., Number for numeric literals, String for string literals).
  • Binary Operations: Validate that both operands of the binary operation have compatible types (e.g., Number + Number).
  • Identifiers: Check that a variable or function has been declared in the current scope.

Function and Parameter Checking

When type checking a function:

  1. Parameter Types: The TypeChecker verifies that the function’s parameters match the expected types.
  2. Return Type: The function’s body is checked, and the return type is validated against the function’s declared return type (or inferred if not explicitly provided).

Assignment and Identifier Checks

In assignment operations, the TypeChecker verifies that the left-hand side (the variable) can hold the type of the right-hand side (the value).

Design Considerations

The TypeChecker was designed with the following goals in mind:

  1. Type Safety: Guarantee that all type-related errors are caught before code generation.
  2. Performance: Efficiently traverse and check large ASTs without unnecessary re-checks.
  3. Extensibility: Allow for future type system extensions (e.g., support for new data types) with minimal changes to the TypeChecker.

Key Design Choices:

  • Single-pass Type Checking: The TypeChecker walks the AST once, checking each node as it encounters it.
  • Hoisting of Declarations: Function and variable declarations are “hoisted” to ensure they are available for checking in the correct scope.

Example Workflow

Type Checking a Simple Program

Consider the following Theta code:

add<Function<Number, Number, Number>> = (x<Number>, y<Number>) -> {
    return x + y
}

...

result<Number> = add(5, 10)

The TypeChecker processes this as follows:

  1. Function Declaration: The TypeChecker validates the add function, ensuring that both parameters are of type Number and that the return type is also Number.
  2. Binary Operation: Inside the function, the x + y expression is checked to ensure both x and y are of type Number.
  3. Function Invocation: The call to add(5, 10) is checked to ensure that both arguments match the expected parameter types (Number).
  4. Assignment: The result of add(5, 10) is assigned to result, and the TypeChecker ensures that result is correctly typed as Number.