[Agda] Infix in Modules with Parameters

[Jacques Carette]

On 2018-04-19 8:48 AM, Dr. ERDI Gergo wrote:
> On Thu, 19 Apr 2018, Philip Wadler wrote:
>
>> 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