generic-reuse

Generic Zero-Cost Reuse for Dependent Types

Cedille code accompanying the paper draft (available on arXiv) authored by Larry Diehl, Denis Firsov, and Aaron Stump. The main repository for this development is here.

This is the generic version of our previous manual reuse work, where identity functions are defined via definitional equality, rather than propositional equality.

We describe the directories containing our code below. As in the paper, program reuse corresponds to non-dependent function type reuse, proof reuse corresponds to dependent function type reuse, and data reuse corresponds to fixpoint type reuse.

GenericReuse

This directory includes our primary contributions, the generic zero-cost reuse combinators for the following types:

• Functions (forgetful allArr2arr & allPi2pi)
• Functions (enriching arr2allArrP & pi2allPiP)
• Fixpoints (forgetful ifix2fix)
• Fixpoints (enriching fix2ifix & fix2ifixP)

The auxiliary combinators also appear here.

Examples

This directory includes reuse examples via our combinators:

• Program Reuse of append and Proof Reuse of associativity
  • forgetful appV2appL & enriching appL2appV
  • forgetful assocV2assocL & enriching assocL2assocV
• Data Reuse of vectors and lists
  • Forgetful v2l
  • Enriching l2v
• Data Reuse of unchecked/raw and checked/typed STLC terms
  • Forgetful t2r
  • Enriching r2tP
• Program Reuse of STLC step function (enriching stepR2stepT)
• Program Reuse of STLC substitution function (enriching subR2subT)

Datatypes

This directory includes the algebraic list and vector datatypes, and their schemes, defined using generic Mendler-style fixpoints:

• Lists Scheme (ListF)
• Lists (List)
• Vectors Scheme (VecF)
• Vectors (Vec)
• Raw Terms Scheme (RawF)
• Raw Terms (Raw)
• Typed Terms Scheme (TermF)
• Typed Terms (Term)

The derived definition of Nat (in terms of the scheme NatF) also appears here, as well the types Tp of STLC (and their scheme TpF).

IndexedMendlerInduction

This directory imports the generic datatype development (via efficient Mendler-style fixpoints) by Firsov et al.:

• Non-Indexed Fixpoints (FixIndM)
• Indexed Fixpoints (IFixIndM)
• Identity Mappings (IIdMapping)

It also includes the generic derivation of induction (iindFixIndM), as well as other technical devices.

Base

This directory includes base or "prelude" definitions, like the Unit and Sigma types. It also includes IdDep, the type of dependent identity functions.