<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 30, 2017 at 9:32 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">A module is the (not always happy) combination of a name space and a list of hypotheses (module telescope).<br>
<br>
I also wish we could open a record value r just by<br>
<br>
  open r<br>
<br>
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.<br>
</blockquote><div><br></div><div>This is a good technical reason.<br> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This is why you have to write<br>
<br>
  open R r<br>
<br>
Note that "R r" is just application of the module R to term r.<br>
<br>
Maybe what confuses you is that for each record type there is a record module with the same name?<br></blockquote><div><br></div><div>This does not have any practical significance other than showing that the way we open records derives from the general rule.<br><br></div><div>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.<br><br></div><div>ex. <br><br></div><div>"record Pair : Set where"<br><br></div><div>creates the module :<br><br></div><div>"module Pair (p : Pair) where"<br></div><div><br><a href="https://agda.readthedocs.io/en/v2.5.2/language/record-types.html#record-modules">https://agda.readthedocs.io/en/v2.5.2/language/record-types.html#record-modules</a><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
Best,<br>
Andreas<div><div class="gmail-h5"><br>
<br>
On 30.03.2017 17:24, Apostolis Xekoukoulotakis wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div class="gmail-h5">
If the module is a record, we use<br>
<br>
"open Pair p"<br>
<br>
If it is a simple module<br>
<br>
"open B"<br>
<br>
if it is a parametrized module<br>
<br>
"module C = B a<br>
 open C"<br>
<br>
or<br>
<br>
"open module C = B a"<br>
<br>
<br>
I find that all these different ways to open a module complicate things.<br>
I would prefer if there was a single concept and that reflected into a<br>
uniform way of opening a module.<br>
<br>
For example, every module is a record.<br>
A parametrized module is a parametrized record.<br>
<br>
And omit "Pair". Just write:<br>
"open p"<br>
<br>
or<br>
<br>
"open (p a)".<br>
<br>
<br></div></div>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br><span class="gmail-HOEnZb"><font color="#888888">
</font></span></blockquote><span class="gmail-HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel  <><      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/%7Eabela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a><br>
</font></span></blockquote></div><br></div></div>