implement binding application

docs/source/reference/binding-application.rst

@@ -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.

libs/contrib/Text/Parser.idr

@@ -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

src/Compiler/Common.idr

@@ -148,7 +148,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/Core/Binary.idr

@@ -25,7 +25,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/Context.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
@@ -322,10 +323,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
@@ -349,6 +351,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
@@ -831,6 +834,8 @@ HasNames Error where
   full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
           <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates
+  full gam (BindingApplicationMismatch fc used bind others)
+      = BindingApplicationMismatch fc used <$> traverse (full gam) bind <*> traverse (full gam) others
 
   resolved gam (Fatal err) = Fatal <$> resolved gam err
   resolved _ (CantConvert fc gam rho s t)
@@ -930,7 +935,8 @@ HasNames Error where
   resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
           <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates
-
+  resolved gam (BindingApplicationMismatch fc used bind others)
+      = BindingApplicationMismatch fc used <$> traverse (resolved gam) bind <*> traverse (resolved gam) others
 export
 HasNames Totality where
   full gam (MkTotality t c) = pure $ MkTotality !(full gam t) !(full gam c)
@@ -1371,6 +1377,7 @@ addBuiltin n ty tot op
          , namedcompexpr = Nothing
          , sizeChange = []
          , schemeExpr = Nothing
+         , bindingMode = NotBinding
          }
 
 export

src/Core/Context/Context.idr

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

src/Core/Context/Data.idr

@@ -97,7 +97,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
@@ -116,7 +116,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/Core.idr

@@ -178,6 +178,12 @@ data Error : Type where
          FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
          -- left: backticked, right: op symbolds
          (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error
+     BindingApplicationMismatch :
+       FC ->
+       (bindingUsed : BindingModifier) ->
+       (bindingCandidates : List Name) ->
+       (nonBindingCandidates : List Name) ->
+       Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
@@ -419,6 +425,8 @@ Show Error where
   show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
        ++ " but used as a " ++ show actual ++ " operator"
+  show (BindingApplicationMismatch fc used binding notBinding)
+       = show fc ++ ": Application used \{show used} syntax but no such function exists"
 
 export
 getWarningLoc : Warning -> FC
@@ -511,6 +519,7 @@ getErrorLoc (InRHS _ _ err) = getErrorLoc err
 getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
 getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn)
 getErrorLoc (OperatorBindingMismatch loc _ _ _ _ _) = Just loc
+getErrorLoc (BindingApplicationMismatch loc _ _ _) = Just loc
 
 export
 killWarningLoc : Warning -> Warning
@@ -603,7 +612,8 @@ killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs
 killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn)
 killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
              = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates
-
+killErrorLoc (BindingApplicationMismatch _ a b c)
+  = BindingApplicationMismatch emptyFC a b c
 
 -- Core is a wrapper around IO that is specialised for efficiency.
 export
@@ -897,6 +907,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))

src/Core/FC.idr

@@ -230,3 +230,4 @@ Pretty Void FC where
   pretty (MkVirtualFC ident startPos endPos) = byShow ident <+> colon
                  <+> prettyPos startPos <+> pretty "--"
                  <+> prettyPos endPos
+

src/Core/Name/Namespace.idr

@@ -300,3 +300,4 @@ dpairNS = mkNamespace "Builtin.DPair"
 export
 natNS : Namespace
 natNS = mkNamespace "Data.Nat"
+

src/Core/Options/Log.idr

@@ -106,6 +106,7 @@ knownTopics = [
     ("elab.as", Nothing),
     ("elab.bindnames", Nothing),
     ("elab.binder", Nothing),
+    ("elab.bindApp", Just "Elaborating binding application"),
     ("elab.case", Nothing),
     ("elab.def.local", Nothing),
     ("elab.delay", Nothing),

src/Core/Reflect.idr

@@ -8,6 +8,7 @@ import Core.Normalise
 import Core.Value
 
 import Libraries.Data.WithDefault
+import Libraries.Data.WithData
 
 %default covering
 
@@ -883,6 +884,13 @@ Reflect a => Reflect (WithFC a) where
            val' <- reflect fc defs lhs env value.val
            appCon fc defs (reflectiontt "MkFCVal") [Erased fc Placeholder, loc', val']
 
+export
+Reflect BindingModifier where
+  reflect fc defs lhs env NotBinding = getCon fc defs (reflectiontt "NotBinding")
+  reflect fc defs lhs env Autobind = getCon fc defs (reflectiontt "Autobind")
+  reflect fc defs lhs env Typebind = getCon fc defs (reflectiontt "Typebind")
+
+
 {-
 -- Reflection of well typed terms: We don't reify terms because that involves
 -- type checking, but we can reflect them