Typing rules for Fun and Core are introduced, emphasizing type soundness and the preservation of typeability in the translation between the two. Both languages utilize the same constructors for types within their typing contexts, indicated by annotations of producer and consumer variables. Data types like Pair and List, as well as codata types such as LPair and Stream, have specialized rules, although typical programming languages would utilize type declarations to check types. The environment is assumed to provide necessary type declarations throughout the rules.
We specialize the rules for data types to the concrete types Pair and List, and the rules for codata types to LPair, Stream and functions 𝜎 → 𝜏.
A realistic programming language would use type declarations introduced by the programmer to typecheck data and codata types instead of using these special cases.
In all of the typing rules below we assume that we have a program environment which contains type declarations for all the definitions contained in the program.
The language Fun only has one syntactic category, terms, so we only need one typing judgment Γ ⊢ t : τ.
Collection
[
|
...
]