[Agda] Open modules and hard to predict normal forms

[Andrea Vezzosi]

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

    postulate
       A : Set
       I : Set

    module R (_ : I)  where
      postulate
        f : A

    postulate
      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
issue.

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.


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