[Agda] Open modules and hard to predict normal forms

Andrea Vezzosi sanzhiyan at gmail.com
Wed Aug 14 07:31:15 CEST 2013

Hi all,

making extensive use of parametrized modules and records, I'm wondering
what's the proper mental model to predict how the normal forms of applied
field selectors will show up, or maybe a summary of how this feature is
implemented and where to look for it in the source.

My question is general, but I'll also add an example for concreteness:

    module Use where

       A : Set
       I : Set

    module R (_ : I)  where
        f : A

      r : I
      X : I -> I
      Q : A -> Set

    module Qualified where
      K = X r
      open R K

      foo : Q f
      foo = { }0 -- normal form: Q (R.f (X r))

    module UnQualified where

      open R (X r)

      foo : Q f
      foo = { }1 -- normal form: Q f

It's fairly counterintuitive that going through a simple definition like K
alters the result, is it because we've gone through a reduction expanding K
during normalization? But, as I said, I've little intuition over the whole

By the way, I've used the terms "qualified" and "unqualified" but the
concern is really about not showing the parameters which I've opened the
module with.

My use cases tend to also include some rerouting of parameters that might
make the reconstruction of the unqualified form harder:

  module X {A} {B} = Product (products A B)
  open X

at this point we usually get normal forms like `Product.someField (products
A B) ...` rather than `someField ...` which is especially unreadable for
mixfix operators because of how the value of the record takes the place of
the first underscore in the name.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130814/9ae9d86a/attachment.html

More information about the Agda mailing list