add operator documentation

docs/source/reference/index.rst

@@ -22,6 +22,7 @@ This is a placeholder, to get set up with readthedocs.
    records
    literate
    overloadedlit
+   operators
    strings
    pragmas
    builtins

docs/source/reference/operators.rst

@@ -5,8 +5,8 @@ Operators
 *********
 
 Idris2 does not have syntax blocs (like in Idris1) or mixfix operators (like in Agda).
-Instead, it expands on the ability of infix operators to enable library designers
-to write DSL while keeping error messages under control.
+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.
@@ -43,9 +43,9 @@ It starts with a fixity keyword, you have the choice to use either ``infixl``,
 ``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.
+brackets are mandatory. Here, we chose for ``+`` to be left-associative, hence ``infixl``.
 
-The number afterwards indicate the *precedence* of the operator, that is, if it should
+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 ``+`` , because of this, we define it like this:
 
@@ -55,9 +55,71 @@ we want ``*`` to *take precedence* over ``+`` , because of this, we define it li
 
 This way, the expression ``n + m * x`` is correctly interpreted as ``n + (m * x)``.
 
+Fixities declarations are optional and only change how a file is parsed, but you can
+use any function defined with operator symbols with parenthesis around it:
+
+.. code-block:: idris
+
+   -- 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:
+
+.. code-block:: idris
+
+   module A
+   export infixl 8 -
+
+.. code-block:: idris
+
+   module B
+   export infixr 5 -
+
+.. code-block:: idris
+
+   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``:
+
+.. code-block:: idris
+
+   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``.
@@ -89,26 +151,33 @@ looks like
    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 for the field that takes a value of the record as the first
-argument, making it unsuitable for use as a binary operator.
+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.
 
 .. code-block:: idris
 
 
    infixl 7 <@>
+
    record SomeRelation (a : Type) where
      (<@>) : a -> a -> Type
-     compose : (x, y, z : a) -> x <@> y -> y <@> z -> x <@> z
+     -- 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
 
@@ -126,7 +195,7 @@ argument:
 
    record SomeRelation (a : Type) where
      (<!@>) : a -> a -> Type
-     compose : (x, y, z : a) -> x <!@> y -> y <!@> z -> x <!@> z
+     compose : {x, y, z : a} -> x <!@> y -> y <!@> z -> x <!@> z
 
    export
    (<@>) : (rel : SomeRelation a) => a -> a -> Type
@@ -170,7 +239,102 @@ right-associative.
 Typebind Operators
 ==================
 
+In dependently-typed programming, we have the ability define types which
+first argument is a type and the second is a lambda using the first argument
+as it's type. A typical example of this is the dependent linear arrow:
+
+ .. code-block:: idris
+
+    infixr 0 =@
+    0 (=@) : (x : Type) -> (x -> Type) -> Type
+    (=@) x f = (1 v : x) -> f v
+
+
+However, we cannot use as is because the second argument is
+a lambda, and writing out any value using this operator will look a bit awkward:
+
+.. code-block:: idris
+
+   linearSingleton : Nat =@ (\x => Singleton x)
+   linearSingleton = ...
+
+What we really want to write, is something like the dependent arrow ``->`` but
+for linear types:
+
+.. code-block:: idris
+
+   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.
+
+.. code-block:: idris
+
+   typebind infixr 0 =@
+
+``typebind`` is a mofidier 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, but
+sometimes, there is no dependency between the first argument, and the expression
+on the right side of the operator. For those case, 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:
+
+.. code-block:: idris
+
+    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 is not given
+by the first argument. For this we use ``:=`` instead of ``:``:
+
+.. code-block:: idris
+
+    autobind infixr 0 =>>
+    (=>>) : Value -> (Value -> Value) -> Value
+    (=>>) = VPi
+
+
+    sig : Value
+    sig =
+        (fstTy := VStar) =>>
+        (sndTy := (_ := fstTy) =>> VStar) =>>
+        (val1 := fstTy) =>>
+        (val2 := sndTy `vapp` val1) =>>
+        VSgima 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.