add some documentation

Author: andrevidela

docs/source/reference/binding-application.rst

@@ -0,0 +1,107 @@
+
+.. _binding:
+
+*********
+Binding Application
+*********
+
+Binding application allows to overload the syntax of function application to better express the
+semantics of dependent types. Take for example the mathematical notation for Sigma-types:
+:math:`\Sigma x \in \mathbb{N} . Fin\ x` it binds the variable ``x`` and makes it available in the
+scope after the dot. Another example is the mathematical notation for ``forall``:
+:math:`\forall x \in \mathbb{N} | p x` it states that for all values ``x`` in the set of natural
+number, the property ``p`` holds.
+
+Without any additional syntactic help those two types are only expressible using a lambda:
+
+.. code-block:: idris
+    record Sigma (a : Type) (p : a -> Type) where
+      fst : a
+      snd : p fst
+
+    record Pi (a : Type) (p : a -> Type) where
+      fn : (x : a) -> p x
+
+    sigmaExample : Sigma Nat (\n => Vect n Int)
+
+    piExample : Pi Nat (\n => Vect n Int)
+
+
+Ideally, instead of relying on a lambda, we would like to write something closer to the original
+mathematical notation, binding application allows the following syntax:
+
+.. code-block:: idris
+    sigmaExample' : Sigma (n : Nat) | Vect n Int
+
+    piExample' : Pi (n : Nat) | Vect n Int
+
+Binding Types
+=============
+
+There are two way to use the binding application, the most common one is to bind a type to a name. If
+we take our ``Sigma`` example again it means that we need to tell the compiler that the type
+constructor can be used with binding syntax. We do this by annotating the type declaration with
+the ``typebind`` keyword.
+
+
+.. code-block:: idris
+   typebind
+   record Sigma (a : Type) (p : a -> Type) where
+     constructor MkSigma
+     fst : a
+     snd : p fst
+
+
+We can also annotate functions with the same keyword, for example the following alias is allowed:
+
+.. code-block:: idris
+   typebind
+   Σ : (a : Type) -> (p : a -> Type) -> Type
+   Σ = Sigma
+
+In the implementation of this function we've used the ``Sigma`` type-constructor without any binding
+syntax. That is because marking something as binding does not stop them from using them with regular
+function application, for example the following is allowed:
+
+.. code-block:: idris
+   -- binding syntax
+   s1 : Sigma (n : Nat) | Fin n
+   s1 = ...
+
+   -- pointfree notation is allowed
+   s2 : Sigma Nat Fin
+   s2 = ...
+
+   s3 : (Nat -> Type) -> Type
+   s3 = Sigma Nat -- partial application is allowed
+
+
+We've seen that you can annotate functions and type constructors, you can also annotate data-constructors. For example, to annotate a record constructor add the keyword before the `constructor` keyword:
+
+.. code-block:: idris
+   record Container where
+     typebind
+     constructor MkCont
+     goal : Type
+     solution : goal -> Type
+
+   ListCont : Container
+   ListCont = MkCont (n : Nat) | Fin n
+
+You can also annotate constructors for data:
+
+.. code-block:: idris
+   data Desc : Type where
+     -- normal constructors
+     One : Desc
+     Ind : Desc -> Desc
+
+     -- binding data constructor
+     typebind
+     Sig : (s : Type) -> (s -> Desc) -> Desc
+
+
+Binding Arbitrary Values
+========================
+
+