This is the source code for my master thesis 'Generic programming with ornaments and dependent types'. The compiled pdf's can be found at my website sijsling.com.
This repository includes a lot of things that have not made it to my thesis. The final library that is presented in my thesis is in the src/Cx folder, and src/Common.agda is used as well. The folder src/Thesis contains code in the thesis that is not directly taken from the actual library. Per section, we indicate where the corresponding Agda code can be found:
- 1 Introduction (Thesis/Introduction.agda)
- 2 Usage (Thesis/Usage.agda)
- 3 Generics and ornaments (Thesis/Sop.agda)
- 3.1 Descriptions
- 3.2 Maps and folds
- 3.3 Ornaments
- 3.4 Ornamental algebras
- 3.5 Discussion
- 3.5.1 Σ-descriptions (Thesis/SigmaDesc.agda)
- 3.5.2 Finding the right ornaments
- 4 Ornaments on dependently typed descriptions (Thesis/Simple.agda)
- 4.1 Contexts and environments (Thesis/SimplifiedContexts.agda)
- 4.2 Descriptions (Cx/Simple/Desc.agda)
- 4.3 Ornaments (Cx/Simple/Ornament.agda)
- 5 Ornaments on families of datatypes (Thesis/Extended.agda)
- 5.1 Descriptions (Cx/Extended/Desc.agda)
- 5.2 Ornaments (Cx/Extended/Ornament.agda)
- 5.3 Algebraic ornaments (Cx/Extended/AlgebraicOrnament.agda)
- 5.4 Discussion
- 5.4.1 Separating parameters from contexts (Thesis/SeparateContexts.agda)
- 6 Generic programming with descriptions (Thesis/Named.agda)
- 6.1 Descriptions and ornaments (Cx/Named/Desc.agda, Cx/Named/Ornament.agda, Cx/Named/AlgebraicOrnament.agda)
- 6.2 Quoting datatypes (Cx/Quoting.agda)
- 6.3 Deriving an embedding-projection pair (Cx/HasDesc/Derive.agda)
- 6.4 Generic functions (Cx/GenericOperations.agda)
- 6.5 Unquoting descriptions (Cx/Unquoting.agda)
- 6.6 Higher-level ornaments (Cx/Named/MoreOrnaments.agda)
- 6.6.1 Structure-preserving ornaments
- 6.6.2 Ornament composition
- 6.6.3 More ornaments
- 6.6.4 Reornaments (Cx/Named/AlgebraicOrnaments.agda)
- 6.7 Discussion
- 6.7.1 Embedding-projection instances
- 7 Discussion (Thesis/Discussion.agda)
- 7.1 Explicit parameter use (Thesis/DiscussionTermLang.agda)
- 7.2 Induction-recursion and strict positivity
- 8 Conclusion
- 8.1 Future work