Binding Application in Idris
I’ve recently implemented binding application as a language feature in Idris. This feature allows writing types such as Dependent pairs in a more ergonomic way without relying on special compiler magic. Or rather, the compiler magic is made available to everyone. This post is a collection of uses for this feature.
This feature is not publicly available yet, but I intend to make it available in the near future.
What is it?
Binding syntax and binding-application is an idea I had a couple of years ago and presented at WITS 2024. It’s a syntactic feature piggybacking on the function-space of a dependent programming language that offers some customisation to the notion of binding. The main use case is to facilitate writing types such as \(\Pi\) or \(\Sigma\) where the second argument is a function dependent on the type given in the first argument. In Idris, one can mark such functions as typebind
because they are meant to bind a type argument, and any such function written f (x : t) | g x
desugars to f t (\x : Type => g x)
This pattern can be generalised to any function with a trailing lambda where the second argument does not necessarily depend on the first. This syntax looks like this f (x <- e) | g x
and desugars to f e (\x : ? => g x)
, those functions are autobind
since the type is automatically inferred.
Let’s move onto the use cases.
Sigma
Dependent pairs, or sigma-types, are ubiquitous in programming with dependent types. If you define your own sigma-type, you have to use a lambda to describe the type of the second projection.
record Sigma (a : Type) (b : a -> Type) where
constructor (&&)
first : a
second : b first
RichList : Type -> Type
RichList a = Sigma Nat (\n => Vect n a) -- lambda here
By marking the type as binding, we can use a much more natural syntactic form.
typebind
record Sigma (a : Type) (b : a -> Type) where
constructor (&&)
first : a
second : b first
RichList : Type -> Type
RichList a = Sigma (n : Nat) | Vect n a
Exists
The Idris base
library has a type called Exists : (a : Type) -> (b : a -> Type) -> Type
which is exactly the same as the dependent pair, except that its first argument is erased. Marking the type as typebind
allows writing Exists (a : Type) | p a
, that syntax enables the natural mathematical reading “There exists a type a
such that p
of a
holds”.
typebind
record Exists (a : Type) (b : a -> Type) where
constructor (-!)
0 index : a
pred : b index
Subset
A similar type exists in base except that the predicate is erased. This type represents values which are constrained by a predicate, but we don’t need to carry the predicate at runtime.
typebind
record Subset (a : Type) (pred : a -> Type) where
constructor (!-)
value : a
0 constraint : pred value
Such a type can be written Subset (x : Nat) | LTE x 9
and can be read “a value x
of type Nat
such that x
is smaller or equal to 9
”
Ornaments
Ornaments are type-descriptors, they contain all the necessary to build types within a dependently-typed programming language. Here is the most basic definitions:
data Orn : (j : Type) -> (j -> i) -> Desc i -> Type where
Say : Inverse e i -> Orn j e (Say i)
Ask : Inverse e i -> Orn j e d -> Orn j e (Ask i d)
Sig : (s : Type) -> {d : s -> Desc i} -> ((sv : s) -> Orn j e (d sv)) -> Orn j e (Sig s d)
Del : (s : Type) -> (s -> Orn j e d) -> Orn j e d
We notice that both Sig
and Del
have the perfect shape for making use of binding application. Therefore, we can rename them and mark them as binding:
data Orn : (j : Type) -> (j -> i) -> Desc i -> Type where
Say : Inverse e i -> Orn j e (Say i)
Ask : Inverse e i -> Orn j e d -> Orn j e (Ask i d)
typebind
Σ : (s : Type) -> {d : s -> Desc i} -> ((sv : s) -> Orn j e (d sv)) -> Orn j e (Sig s d)
typebind
Δ : (s : Type) -> (s -> Orn j e d) -> Orn j e d
Every time we want to use Σ
or Δ
, we can use binding syntax, for example, the ornament decorating the Nat
description into Fin n
makes use of Δ
:
NatD : Desc ()
NatD = Sig (#["Z", "S"]) $ \case
"Z" => Say ()
"S" => Ask () (Say ())
FinO : Orn NatT (const ()) NatD
FinO = Sig (#["Z", "S"]) $ \case
"Z" => Δ (xn : NatT) | Say (Ok (S xn))
"S" => Δ (xn : NatT) | Ask (Ok xn) (Say (Ok (S xn)))
ForAll
Another type in base
is the predicate transformer All : (p : a -> Type) -> (xs : List a) -> Type
. It takes a predicate p
and ensures it holds for every element of the list xs
. There are some cases where writing the predicate is a bit awkward because it cannot be written point-free and requires a lambda. For this, one can use a binding alias:
autobind
ForAll : List a -> (a -> Type) -> Type
ForAll xs p = All p xs
Because the first argument is not a type, we use autobind
instead of typebind
. The syntax also makes clear that we are “iterating” over the list rather than using the list itself as the argument to the predicate.
This enables the syntax:
ForAll (x <- xs) | LTE x 9
Which reads “for all x
in xs
the predicate LTE x 9
holds”
Without the binding syntax, we would have to write the following, which doesn’t read as nicely:
All (\x => LTE x 9) xs
ForSome
In addition to All
there is Any
a predicate transformer that ensures exactly one of the elements in the list satisfies the predicate. The alias can be written in the same way:
autobind
ForSome : List a -> (a -> Type) -> Type
ForSome xs p = Any p xs
And similarly we can write
ForSome (x <- xs) | LTE x 9
With the benefit that it reads nicely as “For some x
in xs
, the predicate LTE x 9
holds”
For-Loops
The most exciting application for me is the fact that we can have idiomatic-looking for-loops in the language.
A for-loop in its C interpretation is a loop defined by three components: An initial state, a break condition, and a state update. This is a very low-level representation of loops, so much so that subsequent languages have abstracted over the notion of loops by relying on iterators. While the details differ from language to language, the general idea remains: An iterator allows iterating over each element once using for
. Here are a few examples where the iterator is xs
:
// python
for x in xs:
body
//scala
for (x <- xs) body
// zig
for (xs) |x| {
body
}
// java
for (x : xs) {
body
}
//rust
for x in xs {
body
}
Back to Idris, it has a function traverse
with the type traverse : Traversable t => Applicative f => (a -> f b) -> t a -> f (t b)
, this type captures the notion that for every “ iterator” t
, we can perform a side-effect f
and return a new list. With binding application we can define for
in Idris as an alias for traverse
.
autobind
for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b)
for = flip traverse
It enables the following syntax:
xs : List String
xs = ["hello", "world", "!"]
main : IO ()
main = ignore $ for (x <- xs) |
putStrLn x
Which mimics the syntax used in other programming languages to iterate on a list. ignore
discards the result of the iteration.
Enjoy Reading This Article?
Here are some more articles you might like to read next: