Leveling Up Dependent Types

Agda source code accompanying the paper (DTP 2013):

Leveling Up Dependent Types - Generic programming over a predicative hierarchy of universes. (Draft)

Code from the paper

• Paper.Background
  • A typical, IR dependently typed universe without a hierarchy.
  • Section 2 of the paper.
• Paper.FixedHierarchy
  • A dependently typed universe with some base types and a universe hierarchy.
  • The generic definition of show.
  • Sections 4 and 5 of the paper.
• Paper.HList
  • The hierarchical universe, extended with the large type Hlist.
  • The generic definition of show.
  • Section 6 of the paper.
• Paper.OriginalDesc
  • The original Desc construction as given by Chapman et al.
  • Uses the large argument Set.
  • Section 7.1 of the paper.
• Paper.ExtensibleHierarchy
  • The hierarchical universe, extended with the Desc construction.
  • The generic definitions of show, double, and δouble.
  • The generic interfaces Generic and GenericΔ.
  • Sections 7, 8, 9 and 10 of the paper.

The underlying type system

• TT.DenotationalTerms
  • A denotational semantics for terms, or terms with an implicit context.
• TT.OperationalTerms
  • An operational semantics for terms, or terms with an explicit context.
  • This extends McBride's type-safe syntax and evaluation to include a universe hierarchy.
  • Compared to McBride's types and terms, here the types and terms (and descriptions) are in a single grammar/datatype.

Extra examples of generic functions over indexed types

• Extras.FixedHierarchy
  • A fixed dependently typed universe with some indexed types in it.
  • Contains examples of applying a generic double over indexed types. Applying generic functions to dependent types changes the result type, prefixing them by Π's that act as "preconditions" that are used to preserve type correctness.
  • Generically double the dependent function `fun and get results out by satisfying its generated preconditions.
  • Generically double the dependent pair `pair and get results out by satisfying its generated preconditions.
• Extras.FixedHierarchyEverywhere WARNING: CONTAINS OMGBBQ AWESOME!
  • Mostly the same as Extras.FixedHierarchy.
  • Defines the fully-generic mapping combinator every.
  • Apply every to a simple double function, and the double function will be applied to nested values on your behalf!
  • The same fun and pair examples are given, but using the new every combinator.