implement binding application

Author: andrevidela

CHANGELOG_NEXT.md

@@ -67,6 +67,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   customise the syntax of operator to look more like a binder.
   See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
 
+* Autobind and Typebind modifiers on functions, type constructors and
+  data constructors allow the user to overload function application to
+  look like a binder. See [#3582](https://github.com/idris-lang/Idris2/issues/3582)
+
 * Fixity declarations without an export modifier now emit a warning in peparation
   for a future version where they will become private by default.
 

CITATION.cff

@@ -0,0 +1,172 @@
+
+.. _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
+=============
+
+The first way to use binding application 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
+
+
+The type constructor can now be called with this syntax: ``Sigma (n : Nat) | Vect n Int``. And it reads
+"Sigma ``n`` of type ``Nat`` such that ``Vect n Int``. This reading is appropriated from the
+mathematical notation :math:`\forall x \in \mathbb{N} | p x` which reads the same.
+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 from our alias
+   s1 : ∃ (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 application is a desugaring that takes an input of the form ``expr1 (name : type) | expr2``
+and maps it to a program ``expr1 type (\name : Type => expr2)``. Binding application will disambiguate
+between binding and non-binding calls for example, the following works:
+
+.. code-block:: idris
+   namespace E1
+     export
+     record Exists (a : Type) (p : a -> Type) where
+
+   namespace E2
+     export typebind
+     record Exists (a : Type) (p : a -> Type) where
+
+   ok : Exists (n : Nat) | Vect n a
+
+
+The compiler will automatically pick ``Exists`` from ``E2`` because the other one is not marked as
+binding. However, when using regular function application, the call must be disambiguated:
+
+.. code-block:: idris
+   failing
+     noOK : Exists Nat Fin
+
+   unambiguous : E1.Exists Nat Fin
+
+
+
+Binding Arbitrary Values
+========================
+
+Sometimes, we still want to using binding application syntax, but we are not binding a type. In those
+cases you want to use the ``autobind`` feature to infer the type of the value being bound. The keyword
+works in the same places as the ``typebind`` keyword, that is:
+
+On type constructors
+
+.. code-block:: idris
+   autobind
+   record StringProp : (str : String) -> (String -> Type) -> Type where
+
+   autobind
+   data MaybeProp : (m : Maybe a) -> (a -> Type) -> Type where
+
+On data constructor:
+
+.. code-block:: idris
+
+on functions:
+
+.. code-block:: idris
+   autobind
+   for : (List a) -> (a -> IO ()) -> IO ()
+   for ls fn = traverse fn ls >> pure ()
+
+
+Instead of using ``:`` as a separator, we use ``<-`` and so the last function can be used this way:
+
+.. code-block:: idris
+   main : IO ()
+   main = for (x <- ['a' .. 'z']) |
+              putCharLn x
+
+The desguaring works in a similar way except that the type of the argument in the lambda has to be
+inferred. ``expr1 (name <- expr2) | expr3`` desugars to ``expr1 expr2 (\name : ? => expr3)``.
+
+Like typebind, you can use regular function application and partial application with ``autobind``
+definitions.

docs/source/reference/binding-application.rst

@@ -1,7 +1,7 @@
 module Text.Parser
 
 import Data.Bool
-import public Data.Nat
+import Data.Nat
 import public Data.List1
 
 import public Text.Parser.Core

libs/contrib/Text/Parser.idr

@@ -156,7 +156,7 @@ getMinimalDef (Coded ns bin)
              = MkGlobalDef fc name (Erased fc Placeholder) NatSet.empty NatSet.empty NatSet.empty NatSet.empty mul
                            Scope.empty (specified Public) (MkTotality Unchecked IsCovering) False
                            [] Nothing refsR False False True
-                           None cdef Nothing [] Nothing
+                           None cdef Nothing [] Nothing NotBinding
          pure (def, Just (ns, bin))
 
 -- ||| Recursively get all calls in a function definition

src/Compiler/Common.idr

@@ -30,7 +30,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2025_08_16_00
+ttcVersion = 2025_08_20_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Binary.idr

@@ -10,6 +10,7 @@ import public Core.Name
 import        Core.Options
 import public Core.Options.Log
 import public Core.TT
+import public Core.WithData
 
 import Libraries.Utils.Binary
 import Libraries.Utils.Path
@@ -325,10 +326,11 @@ commitCtxt ctxt
 ||| @vis  Visibility, defaulting to private
 ||| @def  actual definition
 export
-newDef : (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : Scope) ->
+newDef : {default NotBinding bind : BindingModifier} ->
+         (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : Scope) ->
          (ty : ClosedTerm) -> (vis : WithDefault Visibility Private) -> (def : Def) -> GlobalDef
 newDef fc n rig vars ty vis def
-    = MkGlobalDef
+  = MkGlobalDef
         { location = fc
         , fullname = n
         , type = ty
@@ -352,6 +354,7 @@ newDef fc n rig vars ty vis def
         , namedcompexpr = Nothing
         , sizeChange = []
         , schemeExpr = Nothing
+        , bindingMode = bind
         }
 
 -- Rewrite rules, applied after type checking, for runtime code only
@@ -1372,6 +1375,7 @@ addBuiltin n ty tot op
          , namedcompexpr = Nothing
          , sizeChange = []
          , schemeExpr = Nothing
+         , bindingMode = NotBinding
          }
 
 export

src/Core/Context.idr

@@ -177,7 +177,7 @@ Show Def where
 
 public export
 Constructor' : Type -> Type
-Constructor' = AddFC . WithName . WithArity
+Constructor' = AddFC . WithName . WithArity . AddMetadata Bind'
 
 public export
 Constructor : Type
@@ -331,6 +331,7 @@ record GlobalDef where
   namedcompexpr : Maybe NamedDef
   sizeChange : List SCCall
   schemeExpr : Maybe (SchemeMode, SchemeObj Write)
+  bindingMode : BindingModifier
 
 export
 getDefNameType : GlobalDef -> NameType

src/Core/Context/Context.idr

@@ -101,7 +101,7 @@ addData vars vis tidx (MkData con datacons)
          log "declare.data.parameters" 20 $
             "Positions of parameters for datatype" ++ show tyName ++
             ": " ++ show paramPositions
-         let tydef = newDef con.fc tyName top vars con.val (specified vis)
+         let tydef = newDef {bind = con.bind} con.fc tyName top vars con.val (specified vis)
                             (TCon con.arity
                                   paramPositions
                                   allPos
@@ -120,7 +120,7 @@ addData vars vis tidx (MkData con datacons)
     addDataConstructors tag [] gam = pure gam
     addDataConstructors tag (con :: cs) gam
         = do let conName = con.name.val
-             let condef = newDef con.fc conName top vars con.val (specified $ conVisibility vis) (DCon tag con.arity Nothing)
+             let condef = newDef {bind = con.bind} con.fc conName top vars con.val (specified $ conVisibility vis) (DCon tag con.arity Nothing)
              -- Check 'n' is undefined
              Nothing <- lookupCtxtExact conName gam
                  | Just gdef => throw (AlreadyDefined con.fc conName)

src/Core/Context/Data.idr

@@ -890,6 +890,14 @@ namespace Binder
   traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
   traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)
 
+namespace BindingInfo
+  export
+  traverse : (a -> Core b) -> BindingInfo a -> Core (BindingInfo b)
+  traverse f (BindType name type) = BindType <$> f name <*> f type
+  traverse f (BindExpr name expr) = BindExpr <$> f name <*> f expr
+  traverse f (BindExplicitType name type expr)
+    = BindExplicitType <$> f name <*> f type <*> f expr
+
 export
 mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
            ({vars : _} -> Term vars -> Core (Term vars))