[Agda] Many ways to open a module - Is there a reason?

[Apostolis Xekoukoulotakis]

On Thu, Mar 30, 2017 at 9:32 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> A module is the (not always happy) combination of a name space and a list
> of hypotheses (module telescope).
>
> I also wish we could open a record value r just by
>
>   open r
>
> but this is not possible as "open" is a scope operation and scope checking
> is done /before/ type checking.  However, to get the type R of r (which
> tells you the field names), you would need type checking.
>

This is a good technical reason.


> This is why you have to write
>
>   open R r
>
> Note that "R r" is just application of the module R to term r.
>
> Maybe what confuses you is that for each record type there is a record
> module with the same name?
>

This does not have any practical significance other than showing that the
way we open records derives from the general rule.

One could add to the documentation , the module that is created with the
record type, so as to explain that r is a term and "R r" an application.

ex.

"record Pair : Set where"

creates the module :

"module Pair (p : Pair) where"

https://agda.readthedocs.io/en/v2.5.2/language/record-types.html#record-modules


>
> Best,
> Andreas
>
>
> On 30.03.2017 17:24, Apostolis Xekoukoulotakis wrote:
>
>> If the module is a record, we use
>>
>> "open Pair p"
>>
>> If it is a simple module
>>
>> "open B"
>>
>> if it is a parametrized module
>>
>> "module C = B a
>>  open C"
>>
>> or
>>
>> "open module C = B a"
>>
>>
>> I find that all these different ways to open a module complicate things.
>> I would prefer if there was a single concept and that reflected into a
>> uniform way of opening a module.
>>
>> For example, every module is a record.
>> A parametrized module is a parametrized record.
>>
>> And omit "Pair". Just write:
>> "open p"
>>
>> or
>>
>> "open (p a)".
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170330/278d9f7a/attachment.html>