[Agda] Open modules and hard to predict normal forms

[Andrea Vezzosi]

On Wed, Aug 14, 2013 at 11:35 AM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> Hi Andrea,
>
> this feature is called "display form", and you can start looking in
> Syntax/Translation/**InternalToAbstract.hs
>
>
Thanks, I had reached that module but was a bit lost, knowing about
"display form" seems to help.


> 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).
>
>
Ah, yes, there's issue 657 which is pretty much my second example, my first
one seems unreported though, I guess I'll open another issue.

Are you using Agda 2.3.2 or the darcs version?
>
>
I'm using the darcs version, in fact I was referring to the goals I get
from C-u C-u C-c C-t.

Thanks again,
Andrea

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<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/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130814/5d39c0de/attachment.html