Simple and Inductive Types

The List Type

Learning Objectives

  • 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.

DefinitionList TermsFor an element type 𝑇, the empty list term is denoted nil(𝑇). Given terms 𝑡ℎ and 𝑡𝑡, the cons term is denoted cons(𝑡ℎ,𝑡𝑡).To deconstruct a list, we use the list case term lcase(𝑡1,𝑡𝑛,𝑡𝑐) where 𝑡1 is the scrutinee, 𝑡𝑛 is the nil branch, and 𝑡𝑐 is the cons branch. Usually, 𝑡𝑐 is an abstraction taking two arguments (head and tail).DefinitionList Type [𝑇]The formation rule for list types is as follows.𝑇type[𝑇]typeNotationWe write lcase(𝑡1,ℎ.𝑡.𝑡𝑐) for lcase(𝑡1,𝜆ℎ:𝑇.𝜆𝑡:[𝑇].𝑡𝑐) when the cons branch is written with binders.In source syntax this corresponds to the usual case notationlcase𝑡1of|nil⇒𝑡𝑛|consℎ 𝑡⇒𝑡𝑐DefinitionValue (Lists)nil(𝑇) is a value. The term cons(𝑡ℎ,𝑡𝑡) is a value when both 𝑡ℎ and 𝑡𝑡 are values.

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.

DefinitionDynamics of Lists (𝑡⟶CBV𝑡′)𝑡ℎ⟶CBV𝑡′ℎCons1cons(𝑡ℎ,𝑡𝑡)⟶CBVcons(𝑡′ℎ,𝑡𝑡)𝑡𝑡⟶CBV𝑡′𝑡𝑣ℎvalueCons2cons(𝑣ℎ,𝑡𝑡)⟶CBVcons(𝑣ℎ,𝑡′𝑡)𝑡1⟶CBV𝑡′1CaseList1lcase(𝑡1,𝑡𝑛,𝑡𝑐)⟶CBVlcase(𝑡′1,𝑡𝑛,𝑡𝑐)CaseListNillcase(nil(_),𝑡𝑛,𝑡𝑐)⟶CBV𝑡𝑛𝑣ℎvalue𝑣𝑡valueCaseListConslcase(cons(𝑣ℎ,𝑣𝑡),𝑡𝑛,𝑡𝑐)⟶CBV𝑡𝑐𝑣ℎ𝑣𝑡

Typing rules for lists follow the same structure:

  1. nil(T) has type [T].
  2. cons(h, t) has type [T] if h : T and t : [T].
  3. In lcase, both branches must produce the same result type.
DefinitionTyping Rules for Lists (Γ⊢𝑡::𝑇)NilΓ⊢nil(𝑇)::[𝑇]Γ⊢𝑡ℎ::𝑇Γ⊢𝑡𝑡::[𝑇]ConsΓ⊢cons(𝑡ℎ,𝑡𝑡)::[𝑇]Γ⊢𝑡1::[𝑇]Γ⊢𝑡𝑛::𝑈Γ⊢𝑡𝑐::𝑇→[𝑇]→𝑈CaseListΓ⊢lcase(𝑡1,𝑡𝑛,𝑡𝑐)::𝑈

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.

DefinitionList Recursor TermGiven terms 𝑡1,𝑡𝑛,𝑡𝑐, the list recursor is denoted lrec(𝑡1,𝑡𝑛,𝑡𝑐).Intuitively:•𝑡𝑛 is the base result for the empty list.•𝑡𝑐 is the step function for the non-empty case.•In the cons case, 𝑡𝑐 receives head, tail, and the recursive result for the tail. DefinitionDynamics of List Recursor (𝑡⟶CBV𝑡′)𝑡1⟶CBV𝑡′1RecList1lrec(𝑡1,𝑡𝑛,𝑡𝑐)⟶CBVlrec(𝑡′1,𝑡𝑛,𝑡𝑐)RecListNillrec(nil(_),𝑡𝑛,𝑡𝑐)⟶CBV𝑡𝑛𝑣ℎvalue𝑣𝑡valueRecListConslrec(cons(𝑣ℎ,𝑣𝑡),𝑡𝑛,𝑡𝑐)⟶CBV𝑡𝑐𝑣ℎ𝑣𝑡lrec(𝑣𝑡,𝑡𝑛,𝑡𝑐) DefinitionTyping Rule for List Recursor (Γ⊢𝑡::𝑇)Γ⊢𝑡1::[𝑇]Γ⊢𝑡𝑛::𝑈Γ⊢𝑡𝑐::𝑇→[𝑇]→𝑈→𝑈RecListΓ⊢lrec(𝑡1,𝑡𝑛,𝑡𝑐)::𝑈

Lists, Case Matching and Primitive Recursion

0 / 100 points

Implement type inference and call-by-value reduction for list terms as described in the materials.

This pack is fully standalone. Do not depend on earlier exercise packs.

Implement Core Rules

Extend typing and reduction with the list constructors and eliminators:

  • Nil(T)
  • Cons(head, tail)
  • CaseList { scrutinee, if_nil, if_cons }
  • RecList { scrutinee, if_nil, if_cons }

Implement Example Terms

Implement the following top-level functions.

FunctionTypeDescription
is_empty[Bool] -> BoolReturns True on Nil, otherwise False.
head_or_false[Bool] -> BoolReturns the head if non-empty, otherwise False.
append[Bool] -> [Bool] -> [Bool]Appends two lists (use RecList).
negate_all[Bool] -> [Bool]Maps boolean negation over the list.
all_true[Bool] -> BoolReturns True iff all elements are True.

Grading

  • Only infer_type is tested, the individual typing-rule helper methods are not tested directly.
  • Only step_cbv and multistep_cbv are tested, the individual reduction helper methods are not tested directly.
  • The example terms are tested for both typing and behavior.
  • The behavior tests run through multistep_cbv and accept any semantically correct implementation.

← The Sum Type
Recap and Feedback →