[Agda] Infix in Modules with Parameters

[Philip Wadler]

Thanks. Wow, that looks incredibly ugly. When invoking the module, what
would one pass to instantiate the second parameter? Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 18 April 2018 at 20:56, Martin Stone Davis <martin.stone.davis at gmail.com>
wrote:

> 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.
>
> ```agda
> module M1 (_<_ : Set → Set → Set) where
>   postulate
>     A : Set
>     C : (A < A) < A
>
> module M2 (_<_ : Set → Set → Set) (let _<_ = _<_; infixl 5 _<_) where
>   postulate
>     A : Set
>     C : A < A < A
> ```
>
> On 04/18/2018 11:50 AM, Philip Wadler wrote:
>
> Consider the following simple variant of an example in the user manual.
>
> ---
>
> open import Data.List using (List; _∷_; [])
> open import Data.Bool using (Bool; true; false)
>
> module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where
>
>   infix 1 _≤_
>   infix 2 _⊝_
>
>   insert : A → List A → List A
>   insert x [] = x ∷ []
>   insert x (y ∷ ys) with zero ≤ (y ⊝ x)
>   insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
>   insert x (y ∷ ys)    | false = y ∷ insert x ys
>
>   sort : List A → List A
>   sort []       = []
>   sort (x ∷ xs) = insert x (sort xs)
>
> ---
>
> This works fine. But now say I add infix declarations in so I can omit
> parentheses.
>
> ---
>
> open import Data.List using (List; _∷_; [])
> open import Data.Bool using (Bool; true; false)
>
> module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where
>
>   infix 1 _≤_
>   infix 2 _⊝_
>
>   insert : A → List A → List A
>   insert x [] = x ∷ []
>   insert x (y ∷ ys) with zero ≤ (y ⊝ x)
>   insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
>   insert x (y ∷ ys)    | false = y ∷ insert x ys
>
>   sort : List A → List A
>   sort []       = []
>   sort (x ∷ xs) = insert x (sort xs)
>
> ---
>
> This yields the error message:
>
> /Users/wadler/sf/src/extra/ModuleInfix.agda:8,11-14
>> The following names are not declared in the same scope as their
>> syntax or fixity declaration (i.e., either not in scope at all,
>> imported from another module, or declared in a super module): _≤_
>> _⊝_
>> when scope checking the declaration
>>   module Sort (A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)
>>               (zero : A) where
>
>
> Moving the infix declarations before the module yields a similar error
> message.
>
> 1. What is the right way to declare fixity of infix parameters to a module?
> 2. Where is this documented?
>
> Cheers, -- P
>
>
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180419/66b95bd7/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180419/66b95bd7/attachment.ksh>