[Agda] Infix in Modules with Parameters

[Philip Wadler]

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/

[Martin Stone Davis]

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

Post by Philip Wadler
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)
---
/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 list
https://lists.chalmers.se/mailman/listinfo/agda

[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/

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
```
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)
---
/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 list
https://lists.chalmers.se/mailman/listinfo/agda

[Dr. ERDI Gergo]

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

Those lets are not parameters of the module, so if you have e.g.

module X (A : Set) (_≀_ : A → A → Bool)(let _≀_ = _≀_; infix 1 _≀_)(_⊝_ : A → A → A)(let _⊝_ = _⊝_; infix 1 _⊝_)(zero : A) where

you can still instantiate it with four arguments.

[Jacques Carette]

Post by Dr. ERDI Gergo

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

Those lets are not parameters of the module, so if you have e.g.
module X (A : Set) (_≤_ : A → A → Bool)(let _≤_ = _≤_; infix 1
_≤_)(_⊝_ : A → A → A)(let _⊝_ = _⊝_; infix 1 _⊝_)(zero : A) where
you can still instantiate it with four arguments.

Right - this kind of feature is exactly what I was asking about on the
Types list in November 2016 [1].  Definitional extensions in telescopes
are extremely useful.  They are in particular crucial for implementing
'theory morphisms'.  In Agda, this would translate to adaptors between
modules, but as first-class.

Jacques

[1]
http://types-list.seas.upenn.narkive.com/xzbVN1Jx/types-theories-with-first-class-definitional-extensions

[Guillaume Allais]

For the record, this feature request has been around for close to
4 years now: https://github.com/agda/agda/issues/1235

It would indeed be really nice to have such a thing.

Cheers,
--
gallais

Post by Philip Wadler
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)
---
/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 list
https://lists.chalmers.se/mailman/listinfo/agda