[Agda] Open modules and hard to predict normal forms

[Andreas Abel]

Hi Andrea,

this feature is called "display form", and you can start looking in 
Syntax/Translation/InternalToAbstract.hs

Anyhow, I think the discrepancy between Qualified and Unqualified is 
unwanted and deserves a bug report.  There are some bugs on the tracker 
on "display form problems" already (most should be fixed).

Are you using Agda 2.3.2 or the darcs version?

Cheers,
Andreas

On 14.08.13 7:31 AM, Andrea Vezzosi wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/