Egg #4: Agda style records and modules

• Both modules and records can be parameterised but not indexed.
• Modules cannot take other modules as parameters.
  • It does not make sense because every module is both a record type declaration and a definition of the single instance thereof.
  • Hence, if a module takes another module, it can't tell what's in the taken module.

Table of Contents Record definitions Record opening Record Hierarchies Record Instantiation Modules Opening modules

Record definitions

This:

  record IsMagma (M : Type) : Type where
    constructor MkIsMagma   -- or autogenerated if not named
    fields
      (*) : M -> M -> M

should desugar to this:

  record IsMagma : Type -> Type where
    MkIsMagma : ((*) : M -> M -> M) -> IsMagma M

Notes:

• records cannot be indexed, only parameterised
• all parameters must be named (so that we know how to index)
  • IsMagma : Type -> Type where (*) : M -> M -> M won't work because there's no indication that the M is actually the parameter
• we need to deal with infix ops somehow

Record opening

This:

  f = x * y
    where
      open Fin_isMonoid n

should desugar to this:

  f = x * y
    where
      __M0  = Fin_isMonoid n
      (*)   = proj_*     __M0
      unit  = proj_unit  __M0
      assoc = proj_assoc __M0

or, better, if we had pattern-matching where:

  f = x * y
    where
      MkMonoid (*) unit assoc = Fin_isMonoid n

Notes:

• the above works nicely with using, renaming..to, and hiding
• record opening could probably work at top-level, too

Record Hierarchies

You can use the keyword open in record declarations to mark some sub-fields as recursively auto-opening:

  record IsSemigroup : (a : Type) -> Type where
    fields
      open isMagma : IsMagma a  -- opens automatically
      assoc : (a * b) * c = a * (b * c)
  
      someRandomMagma : IsMagma a  -- does not open automatically
  
  f : IsSemigroup a -> ...
  f sg = ... foo * bar ... assoc ...
    where
      open sg  -- automatically opens the underlying isMagma, too
               -- (but not someRandomMagma)

Record Instantiation

In Agda, records can be constructed by explicitly assigning each field. For example we might have an equivalence relation

  record { refl = ...
         ; sym = ...
         ; trans = ... }

It could be nice to borrow this syntax with the obvious desugaring. If the clear ambiguity here is undesired, the explicit syntax could require the type (or constructor) name:

  record IsEquiv { ... }

Modules

This:

  module M (x₁ : τ₁) ... (xₙ : τₙ) where
    f₁ : σ₁
    f₁ = f₁_def
     ...   
    fₙ : σₙ
    fₙ = fₙ_def

should desugar to these two declarations:

  record __M_type : Type where
    MkM : (x₁ : τ₁) -> ... -> (xₙ : τₙ)
          -> (f₁ : σ₁) -> ... -> (fₙ : σₙ)
          -> M_type

  M : (x₁ : τ₁) -> ... -> (xₙ : τₙ) -> __M_type
  M x₁ ... xₙ = MkM f₁_def ... fₙ_def

Some fᵢ_def might need to be hoisted to top-level because they may need to pattern-match.

Opening modules

• A saturated module is a record, which is opened exactly as a regular record.
• An unsaturated module is a function. Let's generalise open to functions, too.
  • The target of the function must be a record.
  • Assuming a module M x y z, the statement open M x adds a λ y z. fᵢ in front of every field fᵢ of the target of the function.