# Type systems

Reconstruct a typing judgment from syntax, annotations, and context. Separate the validity of one judgment from the soundness of a language.

## Definitions

- **Context**: A map assigning types to variables currently in scope.
- **Arrow type**: A function domain and codomain, written A → B.
- **Application rule**: A function may be applied only to an argument matching its domain type.

## Acceptance procedure

1. Walk the term recursively from an empty context.
2. Extend the context when entering an annotated lambda.
3. Construct arrow types for abstractions.
4. At each application, check the argument type and return the codomain.

## Complexity

The syntax-directed checker visits each term node; context lookup and type comparison add implementation-dependent cost.

## Common failure

Being well typed is not, by itself, a proof of preservation or progress.

## Extensions

Add independently checked derivation trees and a broader type grammar.

## Instances

- KL-FCS-004: Type a Boolean identity application — Reconstructed type: Bool
- KL-FCS-018: The Boolean identity function — Reconstructed type: ["arrow", "Bool", "Bool"]
- KL-FCS-019: A curried constant function — Reconstructed type: ["arrow", "Bool", ["arrow", "Bool", "Bool"]]

## References

- https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html