Reference type checker

The reference type checker takes a Deep program and derives its type and effects according to the formal typing rules. It is a direct transcription of the formal typing judgments into Chelis functions over the Deep AST.

How it works

Hull pattern-matches on the Deep AST constructors and applies the corresponding typing rule at each node. The derivation is structural: each subterm is checked recursively, and the types of compound terms follow from the types of their parts exactly as the rules prescribe.

Because the Deep AST is the same representation the compiler uses internally, there is no parsing or deserialization step. Hull receives the same tree the compiler operates on.

Usage

chelis hull check myprogram.deep

Output includes:

• The derived type of the top-level expression.
• The derived effect set.
• On failure: the rule that could not be satisfied, the offending subterm, and the expected vs. actual types at that point.

Comparing against the compiler

The compiler's own type checker (chelis check) should agree with Hull on every well-typed program and on the classification of every ill-typed program. When they disagree, one of two things is true:

1. The compiler has a bug (it accepts or rejects a program the spec does not).
2. The spec has a bug (a rule is misstated or missing a case).

Either way, the disagreement is actionable. Run both checkers on the same file and diff the output to find the divergence point.

Detailed derivation trace

For debugging, request a full derivation tree:

chelis hull check --trace myprogram.deep

This prints every rule application in the derivation, which is useful for understanding exactly where the spec and the compiler part ways.