Operators

Idris2 does not have syntax blocs (like in Idris1) or mixfix operators (like in Agda). Instead, it expands on the abilities of infix operators to enable library designers to write Domain Specific Languages (DSLs) while keeping error messages under control.

Because operators are not linked to function definitions, they are also part of the file namespacing and follow the same rules as other defintions.

Warning

Operators can and will make some code less legible. Use with taste and caution. This document is meant to be mainly used by library authors and advanced users. If you are on the fence about using operators, err on the side of caution and avoid them.

Basics

Before we jump into the fancy features, let us explain how operators work for most users.

When you see an expression

1 + n

It means that there is a function (+) and a fixity declaration in scope. A fixity for this operator looks like this

infixl 8 +

It starts with a fixity keyword, you have the choice to use either infixl, infixr, infix or prefix.

infixl means the operator is left-associative, so that successive applications of the operator will bracket to the left: n + m + 3 + x = (((n + m) + 3) + x)`. Similarly, infixr is right-associative, and infix is non-associative, so the brackets are mandatory. Here, we chose for + to be left-associative, hence infixl.

The number after the fixity indicate the precedence level of the operator, that is, if it should be bracketed before, or after, other operators used in the same expression. For example, we want * to take precedence over + we write:

infixl 9 *

This way, the expression n + m * x is correctly interpreted as n + (m * x).

Fixity declarations are optional and change how a file is parsed, but you can use any function defined with operator symbols with parenthesis around it:

-- those two are the same
n + 3
(+) n 3

Because fixities are separated from the function definitions, a single operator can have 0 or multiple fixity definitions. In the next section, we explain how to deal with multiple fixity definitions.

Fixity & Precedence Namespacing

Sometimes it could be that you need to import two libraries that export conflicting fixities. If that is the case, the compiler will emit a warning and pick one of the fixities to parse the file. If that happens, you should hide the fixity definitions that you do not wish to use. For this, use the %hide directive, just like you would to hide a function definition, but use the fixity and the operator to hide at the end. Let’s work through an example:

module A
export infixl 8 -

module B
export infixr 5 -

module C

import A
import B

test : Int
test = 1 - 3 - 10

This program will raise a warning on the last line of module C because there are two conflicting fixities in scope. Should we parse the expression as (1 - 3) - 10 or as 1 - (3 - 10)? In those cases, you can hide the extra fixity you do not wish to use by using %hide:

module C

import A
import B

%hide A.infixl.(-)

test : Int
test = 1 - 3 - 10 -- all good, no error

In which case the program will be parsed as 1 - (3 - 10) and not emit any errors.

Export modifiers on fixities

Just like other top-level declarations in the language, fixities can be exported with the export access modifier, or kept private with private.

A private fixity will remain in scope for the rest of the file but will not be visible to users that import the module. Because fixities and operators are separate, this does not mean you cannot use the functions that have this operator name, it merely means that you cannot use it in infix position. But you can use it as a regular function application using brackets. Let us see what this looks like

module A

private infixl &&& 8

-- a binary function making use of our fixity definition
export
(&&&) : ...

module B

import A

main : IO ()
main = do print (a &&& b) -- won't work
          print ((&&&) a b) -- ok

In what follows, we have two examples of programs that benefit from declaring a fixity private rather than export.

Private record fixity pattern

Private fixity declarations are useful in conjuction with records. When you declare a record with operators as fields, it is helpful to write them in infix position. However, the compiler will also synthesize a projection function for the field that takes as first argument the a value of the record to project from. This makes using the operator as a binary infix operator impossible, since it now has 3 arguments.

infixl 7 <@>

record SomeRelation (a : Type) where
  (<@>) : a -> a -> Type
  -- we use the field here in infix position
  compose : {x, y, z : a} -> x <@> y -> y <@> z -> x <@> z

lteRel : SomeRelation Nat
lteRel = ...

-- we want to use <@> in infix position here as well but we cannot
natRel : Nat -> Nat -> Type
natRel x y = (<@>) lteRel x y

What we really want to write is natRel x y = (<@>) x y but (<@>) now has type SomeRelation a -> a -> a -> Type.

The solution is to define a private field with a private fixity and a public one which relies on proof search to find the appropriate argument:

private infixl 7 <!@>
export  infixl 7 <@>

record SomeRelation (a : Type) where
  (<!@>) : a -> a -> Type
  compose : {x, y, z : a} -> x <!@> y -> y <!@> z -> x <!@> z

export
(<@>) : (rel : SomeRelation a) => a -> a -> Type
x <@> y = (<!@>) rel x y

%hint
lteRel : SomeRelation Nat
lteRel = ...

natRel : Nat -> Nat -> Type
natRel x y = x <@> y

We define (<@>) as a projection function with an implicit parameter allowing it to be used as a binary operator once again.

Private Local definition

Private fixity definitions are useful when redefining an operator fixity in a module. This happens when multiple DSLs are imported as the same time and you do not want to expose conflicting fixity declarations:

module Coproduct

import Product

-- mark this as private since we don't want to clash
-- with the Prelude + when importing the module
private infixr 5 +

data (+) : a -> a -> Type where
  ...

distrib1 : {x, y, z : a} -> x + y + z -> (x + y) + z

Here distrib1 makes explicit use of the operator being defined as right-associative.

Typebind Operators

In dependently-typed programming, we have the ability define constructors which first argument is a type and the second is a type indexed over the first argument. A typical example of this is the dependent linear arrow:

infixr 0 =@
0 (=@) : (x : Type) -> (x -> Type) -> Type
(=@) x f = (1 v : x) -> f v

However, when trying to use it in infix position, we have to use a lambda to populate the second argument:

linearSingleton : Nat =@ (\x => Singleton x)
linearSingleton = ...

What we really want to write, is something like the dependent arrow -> but for linear types:

linearSingleton : (x : Nat) =@ Singleton x
linearSingleton = ...

The above syntax is allowed if the operator is declared as typebind. For this, simply add the typebind keyword in front of the fixity declaration.

typebind infixr 0 =@

typebind is a modifier like export and both can be used at the same time.

An operator defined as typebind cannot be used in regular position anymore, writing Nat =@ (\x => Singleton x) will raise an error.

This new syntax is purely syntax sugar and converts any instance of (name : type) op expr into type op (\name : type => expr)

Because of its left-to-right binding structure, typebind operators can only ever be infixr with precedence 0.

Autobind Operators

Typebind operators allow to bind a type on the left side of an operator, so that is can be used as the index of the second argument. But sometimes, there is no dependency between the first and second argument, yet we still want to use binding syntax. For those cases, we use autobind.

An example of this is a DSL for a dependently-typed programming language where the constructor for Pi takes terms on the left and lambdas on the right:

VPi : Value -> (Value -> Value) -> Value

sig : Value
sig = VPi VStar                 (\fstTy -> VPi
      (VPi fstTy (const VStar)) (\sndTy -> VPi
      fstTy                     (\val1 -> VPi
      (sndTy `vapp` val1)       (\val2 ->
      VSigma fstTy sndTy)))))

We would like to use a custom operator to build values using VPi, but its signature does not follow the pattern that typebind uses. Instead, we use autobind to tell the compiler that the type of the lambda must be inferred. For this we use := instead of ::

autobind infixr 0 =>>
(=>>) : Value -> (Value -> Value) -> Value
(=>>) = VPi


sig : Value
sig =
    (fstTy := VStar) =>>
    (sndTy := (_ := fstTy) =>> VStar) =>>
    (val1 := fstTy) =>>
    (val2 := sndTy `vapp` val1) =>>
    VSigma fstTy sndTy

This new syntax is much closer to what the code is meant to look like for users accustomed to dependently-typed programming languages.

More technically, any autobind operator is called with the syntax (name := expr) op body and is desugared into expr op (\name : ? => body). If you want, or need, to give the type explicitly, you can still do so by using the full syntax: (name : type := expr) op body which is desugared into expr op (\name : type => body).

Like typebind, autobind operators cannot be used as regular operators anymore , additionally an autobind operator cannot use the typebind syntax either.