Container Compendium
A compilation of work on containers — a data structure with wonderful mathematical properties — with the goal of designing and implementing interactive programs in Idris.
Where to start
This is a non-linear book. Choose the entry point that fits your background:
- New to all of this? Start with Start
- Know dependent types, not category theory? Go to Data.Category
- Know category theory and dependent types? Jump to Data.Container.Monad
- Here for the thesis? Start at Introduction
What is this for?
The target reader has at least two of the following:
- Has written software before, wants to write better software, and has heard about functional programming
- Is interested in understanding the ins-and-outs of programs
- Has heard about “polynomial functors” and wants to see applications
- Is familiar with abstract algebra but finds category theory one step too far
Topics covered
- Containers — shapes, positions, request-response structures
- Category theory in Idris — categories, functors, natural transformations
- Interactive programs — bidirectional lenses, sequent calculus, tactics
- Optics — lenses, prisms, van Laarhoven representation
- Proofs — sigma types, products, extensionality