Modelling bindings consistently in the AST

The bindings proposal introduced the idea of a type for modelling bindings in the AST, and this is now used for case branches:

data CaseBranch' a b
  = CaseBranch
      Name
      -- ^ constructor
      [Bind' a]
      -- ^ constructor parameters.
      -- Ideally this would be '[Bind' (Meta TypeCache)]' since we always know the types of branch
      -- bindings. Unfortunately that breaks generic traversals like '_exprMeta'.
      (Expr' a b)
      -- ^ right hand side
  deriving (Eq, Show, Data, Generic)
  deriving (FromJSON, ToJSON) via VJSON (CaseBranch' a b)

-- | Variable bindings
-- These are used in case branches to represent the binding of a variable.
-- They aren't currently used in lambdas or lets, but in the future that may change.
data Bind' a = Bind a Name
  deriving (Eq, Show, Data, Generic)
  deriving (FromJSON, ToJSON) via VJSON (Bind' a)

Using Bind for all other bindings (λ, Λ, let(rec), ∀) would allow us to do lots of nice things like render them consistently, present binding-specific information in the sidebar, etc.

The reason we haven't done this yet is because it makes it much harder to describe specific locations in the AST using our current zipper design. In a hypothetical AST with Bind everywhere, we will have terms like this:

Ann (LAM (Bind "a") (Lam (Bind "x") (Var "e")) (TForall (Bind "a") KType (TFun (TCon "Nat") (TCon "Nat")))

which represents the following expression

(Λ a. (λx. e)) : ∀a. Nat -> Nat

In this expression we have the following:

a type variable Bind inside an Expr
a term variable Bind inside an Expr
a type variable Bind inside a Type inside an Expr

And we already have:

a case-binding (term variable) Bind inside an Expr

We would need to model each of these separately, as our zipper type isn't powerful enough to be generic through several layers of different types. To illustrate, we currently have four zipper types:

ExprZ for expressions
TypeZ for types inside expressions
TypeZip for types not inside expressions (e.g. type signatures)
CaseBindZ for bindings inside case expressions

There are zippers that can look inside arbitrarily many nested types - notably the lens-based zippers, and my current thinking is that using something like this would remove a lot of this pain. Instead of something like TypeZ we would have Top :>> Expr :>> Type. A binding in a forall in an annotation would be Top :>> Expr :>> Type :>> Bind.

Until we do that or something like it, adding Bind everywhere will make a big mess of the backend code, so I'm quite reluctant to pursue it.

hackworthltd / primer

Modelling bindings consistently in the AST #75