Home/Mathematics/Category Theory and Functional Programming/Types/

Sum Types

100%

Bool

Introduction, elimination and computation rules

Data constructors as functions (morphisms), in this case from the terminal object (since they are nullary).

Enumerations

Big enumerations

Case statement as an enumeration elimination pattern

Pattern matching as an enumeration elimination rule

Nullary data constructors as the enumeration introduction rule

Either

Functions (computation rules) from Either

Maybe

Functoriality/lifting for sum types