Generic Constructors and Eliminators from Descriptions

Agda code for the paper by Larry Diehl and Tim Sheard (WGP 2014):

• Paper draft
• Published paper

Code from the paper

• Background Definitions
  • Enumerations & Tags
  • Descriptions
  • Fixpoints
• Contributed Generic Definitions
  • Un/CurriedBranches
  • Un/CurriedEl
  • Un/CurriedHyps
  • Generic constructor inj
  • Generic eliminator elim
• Examples
  • Vector definitions
  • Vector constructors using primitive init
  • Vector constructors using derived inj
  • Vector concat using primitive ind
  • Vector concat using derived elim
• Correctness
  • Soundness
  • Completeness

Stratified version of code using universe levels

• Background Definitions
  • Enumerations & Tags
  • Descriptions
  • Fixpoints
• Contributed Generic Definitions
  • Un/CurriedBranches
  • Un/CurriedEl
  • Un/CurriedHyps
  • Generic constructor inj
  • Generic eliminator elim
• Examples
  • Vector definitions
  • Vector constructors using primitive init
  • Vector constructors using derived inj
  • Vector concat using primitive ind
  • Vector concat using derived elim
• Correctness
  • Soundness
  • Completeness

Comparing append using ind vs elim

In the paper we broke up the definition of concat using ind into pieces because it was so big, and showed the definition using elim inlined. Here is the definition of a similar function, append, using ind and elim where both definitions are inlined:

• append using ind
• append using elim

Notes

The code is released under an MIT license