FunImplicits.lagda.rst

agda

module FunImplicits where

open import Data.Bool

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

postulate p : true ≡ { Bool } false

postulate p₁ : _≡_ { Bool } true false

For prefix usage, usual rules apply.

-- | Rules for implicit resolution are different
--   for prefix and infix usage 

postulate p₂ : _≡_ { A = Bool } true false

p₃ : Bool → Set
p₃ = true ≡_

p₄ : Bool → Set
p₄ = _≡ false

For infix usage, implicits can be placed to the right of any of the “parts” of the infix operator.

Implicits are place in the leftmost corresponding position. If two implicits are to appear in the same position, then they should be placed in left-to-right order, as they appear in the type signature.

Mixfix operator:             _  X  _  Y  _  Z  _
                                 ↑     ↑     ↑ 
Available positions:             ₁     ₂     ₃

Type signature:          {α} a {β} b {γ} c {δ} d {ε} → T
Assigned positions:       ₁     ₁     ₂     ₃     ₃

p₅ : Bool → Set
p₅ = true ≡_ { Bool }

p₆ : Bool → Set
p₆ = _≡ { Bool } false

postulate _X_ : { A : Set } → A → { B : Set } → B → Set

p₇ = (true X_) zero

-- Pseudo-agda

p₈ = (true X_) {Nat} zero

p₉ = (true X_ {Bool}) {Nat} zero

What if not all the arguments are applied in mixfix notation?

Mixfix operator:             _  X  _  Y_Z_
                                 ↑         ↑ 
Available positions:             ₁         ₂

Type signature:          {α} a {β} b {γ} c {δ} d {ε} → T
Assigned positions:       ₁     ₁     ₂  ___________

Mixfix operator:             _  X_Y     _  Z  _
                                   ↑        ↑      
Available positions:               ₁        ₂     

Type signature:          {α} a {β} b {γ} c {δ} d {ε} → T
Assigned positions:       ₁     ₁ ______    ₂     ₃     ₃

The criterion of where to place implicits can be summarized as:

• Find the closest (left and right) non-implicit arguments in the type signature.

  These arguments correspond to two underscores. This implicit argument should appear to the right of the token that appears between those two underscores.

  If this token appears as a section (i.e. the underscores are spelled-out as part of a token), then the position of the implicit will be moved until the end of the token.

  • Corner cases:
    • There is no left non-implicit argument:
      • Place the implicit argument to the right of the first token of the mixfix operator.
    • There is no right non-implicit argument.
      • Place the implicit argument to the right of the last token of the mixfix operator.
    • There are no non-implicit arguments.
      • This is not a mixfix operator, prefix rules should be applied.