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

[Andreas Abel]

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 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?

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/