Simple and Inductive Types

The Sum Type

Learning Objectives

  • You know the sum type terms (inl, inr, and scase) and their intended meaning.
  • You can derive and implement typing rules for sums.
  • You can implement call-by-value reduction rules for injections and sum case matching.

Introduction

Sum types, as you already know from chapter 1 are useful for lots of situations. For example, when we want a variable to hold one of many different types, we could express that using sum types.

DefinitionInjections and Case Matching TermsThe left and right injection terms are denoted inl(𝑑,𝑇2) and inr(𝑑,𝑇1) respectively.To deconstruct a sum, we use the sum case matching term scase(𝑑1,𝑑𝑙,π‘‘π‘Ÿ) where 𝑑1 represents the scrutinee, 𝑑𝑙 the left case and π‘‘π‘Ÿ the right case. The left and right cases are usually abstractions.DefinitionSum Type (𝑇1+𝑇2)The formation rule for the sum of two types is as follows.𝑇1type𝑇2type𝑇1+𝑇2typeNotationWe use scase(𝑑1,π‘₯.𝑑𝑙,𝑦.π‘‘π‘Ÿ) to denote the case matching term scase(𝑑1,πœ†π‘₯:𝑇1.𝑑𝑙,πœ†π‘¦:𝑇2.π‘‘π‘Ÿ) where the branches are abstractions. The types 𝑇1 and 𝑇2 are the types of the summands where 𝑑1 has type 𝑇1+𝑇2.This notation has a more direct connection to the usual case-of construct, which represents the same term.scase𝑑1of|inl(π‘₯)⇒𝑑𝑙|inr(𝑦)β‡’π‘‘π‘ŸDefinitionValue (Injections)The terms inl(𝑑) and inr(𝑑) are values if 𝑑 is a value.

The dynamics of sum types are straight-forward. We reduce injection terms until they are values. Sum case matching reduces the scrutinee and once it’s an injection, it reduces to the corresponding branch. The types in the injection are not used after type checking so we ignore them (by blanketing them with underscores) during the reduction rules.

DefinitionDynamics of Sums (π‘‘βŸΆCBV𝑑′)π‘‘βŸΆCBV𝑑′Inl1inl(𝑑)⟢CBVinl(𝑑′)π‘‘βŸΆCBV𝑑′Inr1inr(𝑑)⟢CBVinr(𝑑′)𝑑1⟢CBV𝑑′1CaseSum1scase(𝑑1,𝑑𝑙,π‘‘π‘Ÿ)⟢CBVscase(𝑑′1,𝑑𝑙,π‘‘π‘Ÿ)𝑣valueCaseSumLscase(inl(𝑣,_),𝑑𝑙,π‘‘π‘Ÿ)⟢CBV𝑑𝑙𝑣𝑣valueCaseSumRscase(inr(𝑣,_),𝑑𝑙,π‘‘π‘Ÿ)⟢CBVπ‘‘π‘Ÿπ‘£

The rules should seem familiar, because they are very closely related to natural numbers (compare with CaseNat for example).

Typing rules for sums are as follows.

DefinitionTyping Rules for Sums (Ξ“βŠ’π‘‘::𝑇)Ξ“βŠ’π‘‘::𝑇1InlΞ“βŠ’inl(𝑑,𝑇2)::𝑇1+𝑇2Ξ“βŠ’π‘‘::𝑇2InrΞ“βŠ’inr(𝑑,𝑇1)::𝑇1+𝑇2Ξ“βŠ’π‘‘π‘™::𝑇1β†’π‘‡Ξ“βŠ’π‘‘π‘Ÿ::𝑇2β†’π‘‡Ξ“βŠ’π‘‘1::𝑇1+𝑇2CaseSumΞ“βŠ’scase(𝑑1,𝑑𝑙,π‘‘π‘Ÿ)::𝑇

Again, the CaseSum typing rule reminds us of the CaseNat rule.


Injections, Case Matching and The Sum Type

0 / 90 points

Implement type inference and call-by-value reduction for injections and sum case matching as described in the materials.

Note: the macro is brittle with parsing sums, add parentheses around (Bool + Bool) to make sure it’s parsed correctly.

Implement Example Terms

Implement the following terms as top-level functions:

FunctionTypeDescription
swap(Bool + (Bool + Bool)) β†’ ((Bool + Bool) + Bool)Swaps the left and right in the sum.
forward(Bool β†’ Bool) β†’ (Bool + Bool)Forward direction of an equivalence between Bool β†’ Bool and Bool + Bool.
backward(Bool + Bool) β†’ (Bool β†’ Bool)Backward direction of an equivalence between Bool β†’ Bool and Bool + Bool.

forward and backward should be inverses of each other, but only forward after backward, i.e. the identity on Bool + Bool can be tested easily. Comparing two functions of type Bool β†’ Bool requires comparing them one input at a time.

Note: there are many correct solutions to forward and backward.

Hints for forward and backward:

  • forward: call the argument f : Bool -> Bool. Now let a = f true and b = f false.
    • If a = true, then return inl b with a suitable right-hand type
    • If a = false, then return inr b with a suitable left-hand type
  • backward: call the argument s : Bool + Bool.
    • If s = inl l _, then return fun b : Bool, if b then True else l
    • If s = inr r _, then return fun b : Bool, if b then False else r

Try defining the forward and backward functions in STLC++ first to ensure you have right logic.

Grading

  • Only infer_type is tested, the individual typing rules are not.
  • Only step_cbv and multistep_cbv are tested, the individual reduction rules are not.
  • Only the composition of forward after backward is tested for correct behavior. The behavior is tested only via multistep_cbv. The terms can be defined in various different, but correct ways.
  • The example terms are tested for correct typing.

← Pairs and The Product Type
The List Type →