You know the core terms and typing rules for lists in STLC.
You know the call-by-value reduction rules for list constructors and list case matching.
You can implement list typing and dynamics by following the same pattern as products and sums.
Introduction
Lists are a recursive algebraic data type with two constructors:
an empty list and a non-empty list built from a head and a tail.
As with sums and natural numbers, we add both syntax and operational rules to the calculus.
The dynamics of lists are closely related to products and sums:
we first reduce inside constructors, and when the scrutinee becomes canonical (nil or cons), the matching rule applies.
Typing rules for lists follow the same structure:
nil(T) has type [T].
cons(h, t) has type [T] if h : T and t : [T].
In lcase, both branches must produce the same result type.
As with CaseNat and CaseSum, the branch term in CaseList is encoded as an abstraction.
This keeps the core syntax small while still giving us expressive case analysis.
Primitive Recursion on Lists
To define useful recursive list functions (such as append, map, and all) we add a list recursor.
As with lcase, the call-by-value semantics evaluates only the scrutinee before choosing a branch.
In Rust code, this constructor is called RecList.