<div dir="ltr">Thanks. Wow, that looks incredibly ugly. When invoking the module, what would one pass to instantiate the second parameter? Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 18 April 2018 at 20:56, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<p>I'm not sure if or where it's documented, but here's a trick I
use: place a `let` declaration in with the module parameters. See
`M2` below.</p>
<p>```agda<br>
module M1 (_<_ : Set → Set → Set) where<br>
postulate <br>
A : Set<br>
C : (A < A) < A<br>
<br>
module M2 (_<_ : Set → Set → Set) (let _<_ = _<_; infixl
5 _<_) where<br>
postulate <br>
A : Set<br>
C : A < A < A<br>
```<br>
</p><div><div class="h5">
<br>
<div class="m_-1792914237898759271moz-cite-prefix">On 04/18/2018 11:50 AM, Philip Wadler
wrote:<br>
</div>
</div></div><blockquote type="cite"><div><div class="h5">
<div dir="ltr">Consider the following simple variant of an example
in the user manual.
<div><br>
</div>
<div>---<br>
<div><br>
</div>
<div>
<div>open import Data.List using (List; _∷_; [])<br>
</div>
<div>open import Data.Bool using (Bool; true; false)</div>
<div><br>
</div>
<div>module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A →
A)(zero : A) where</div>
<div><br>
</div>
<div> infix 1 _≤_</div>
<div> infix 2 _⊝_</div>
<div><br>
</div>
<div> insert : A → List A → List A</div>
<div> insert x [] = x ∷ []</div>
<div> insert x (y ∷ ys) with zero ≤ (y ⊝ x)</div>
<div> insert x (y ∷ ys) | true = x ∷ y ∷ ys</div>
<div> insert x (y ∷ ys) | false = y ∷ insert x ys</div>
<div><br>
</div>
<div> sort : List A → List A</div>
<div> sort [] = []</div>
<div> sort (x ∷ xs) = insert x (sort xs)</div>
<div><br>
</div>
<div>---</div>
<div><br>
</div>
<div>This works fine. But now say I add infix declarations
in so I can omit parentheses.</div>
<div><br>
</div>
<div>---</div>
<div><br>
</div>
<div>
<div>open import Data.List using (List; _∷_; [])<br>
</div>
<div>open import Data.Bool using (Bool; true; false)</div>
<div><br>
</div>
<div>module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A
→ A)(zero : A) where</div>
<div><br>
</div>
<div> infix 1 _≤_</div>
<div> infix 2 _⊝_</div>
<div><br>
</div>
<div> insert : A → List A → List A</div>
<div> insert x [] = x ∷ []</div>
<div> insert x (y ∷ ys) with zero ≤ (y ⊝ x)</div>
<div> insert x (y ∷ ys) | true = x ∷ y ∷ ys</div>
<div> insert x (y ∷ ys) | false = y ∷ insert x ys</div>
<div><br>
</div>
<div> sort : List A → List A</div>
<div> sort [] = []</div>
<div> sort (x ∷ xs) = insert x (sort xs)</div>
</div>
<div><br>
</div>
<div>---</div>
<div><br>
</div>
<div>This yields the error message:</div>
<div><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">/Users/wadler/sf/src/extra/<wbr>ModuleInfix.agda:8,11-14<br>
The following names are not declared in the same scope
as their<br>
syntax or fixity declaration (i.e., either not in scope
at all,<br>
imported from another module, or declared in a super
module): _≤_<br>
_⊝_<br>
when scope checking the declaration<br>
module Sort (A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A
→ A)<br>
(zero : A) where</blockquote>
</div>
<div><br>
</div>
<div>Moving the infix declarations before the module yields
a similar error message.</div>
<div><br>
</div>
<div>1. What is the right way to declare fixity of infix
parameters to a module?</div>
<div>2. Where is this documented?</div>
<div><br>
</div>
<div>Cheers, -- P</div>
<div><br>
</div>
<div><br>
</div>
<div><br>
</div>
<div><br>
</div>
<div>
<div class="m_-1792914237898759271gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of
Theoretical Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="m_-1792914237898759271mimeAttachmentHeader"></fieldset>
<br>
</div></div><pre>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="m_-1792914237898759271mimeAttachmentHeader"></fieldset>
<br>
<pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-1792914237898759271moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-1792914237898759271moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>