Thesis

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.

Agda sources

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.5.1 Σ-descriptions (Thesis/SigmaDesc.agda)

• 3.5.2 Finding the right ornaments

• 3.1 Descriptions

• 3.2 Maps and folds

• 3.3 Ornaments

• 3.4 Ornamental algebras

• 3.5 Discussion

• 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.4.1 Separating parameters from contexts (Thesis/SeparateContexts.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

• 6 Generic programming with descriptions (Thesis/Named.agda)

• 6.7.1 Embedding-projection instances

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

• 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