locally nameless

1. example implementation in Haskell

categories: abstract syntax

A technique that combines named and nameless variable representations.

The basic idea is that free variables are named, while bound variables are nameless. Specifically, bound variables are represented by de Bruijn indices. (In theory, any nameless representation could work, but de Bruijn indices admit the simplest implementation.)

Advantages:

Since bound variables are nameless, \( \alpha \)-equivalence is just equality.
Substitution has a very simple implementation: \( [x \mapsto t_2]t_1 \) just replaces all occurrences of \( x \) in \( t_1 \) with \( t_2 \). This works for a few reasons.
- Since named variables are always free, we do not need to worry about the usual problems with named variables; i.e., shadowing and capturing.
- Since free variables are always named, we do not need to worry about the usual problems with de Bruijn indices; i.e., shifting. Less pithily: when performing the substitution \( [x \mapsto t_2]t_1 \), we assume that \( t_2 \) is “locally closed”; i.e., all of the bound variables that occur in \( t_2 \) are bound within \( t_2 \). This ensures that \( t_2 \) has the same meaning in any substitution context, which lets us avoid the complicated and tedious shifting operations that de Bruijn-based representations usually deal with.

1. example implementation in Haskell

The type of terms is parameterized by a type a of variable names. There are two constructors for terms that represent variables: BVar for bound variables and FVar for free variables. Abstractions (implicitly) bind indices, not names.

{-# LANGUAGE BlockArguments, LambdaCase, TypeFamilies #-}

import GHC.Generics
import Numeric.Natural
import Data.Functor.Foldable

data Term a
  = BVar Natural
  | FVar a
  | Abs (Term a)
  | App (Term a) (Term a)
  deriving (Generic, Foldable)

Because operations on locally nameless terms are structurally recursive, it makes sense to define them as algebras of a base functor.

data TermF a x
  = BVarF Natural
  | FVarF a
  | AbsF x
  | AppF x x
  deriving (Generic, Functor)

type instance Base (Term a) = TermF a
instance Recursive (Term a)
instance Corecursive (Term a)

In a named representation, we would define \( \beta \)-reduction by saying that \( (\lambda x.t_1) t_2 \) reduces to \( [x \mapsto t_2]t_1 \). Our abstractions are nameless, so this definition does not work. But we can tweak it a little: rather than replacing a name, we simply replace the lowest de Bruijn index. The operation that replaces the lowest de Bruijn index in the term \( t \) with the term \( u \) is called opening, and it is denoted \( t^u \).

open :: Term a -> Term a -> Term a
open u = \t -> cata (flip go) t 0 where
  go j = \case
    BVarF i | i == j -> u
            | otherwise -> BVar i
    FVarF x -> FVar x
    AbsF k -> Abs (k (j + 1))
    AppF k1 k2 -> App (k1 j) (k2 j)

(^^) = flip open

Now we can define \( \beta \)-reduction: \( (\lambda. t_1) t_2 \) reduces to \( {t_1}^{t_2} \).

In a typical de Bruijn index-based implementation, we would have to shift indices around in order to avoid capturing them. The locally nameless representation avoids this by mandating that all terms be locally closed; i.e., that every index is bound by some enclosing binder. In a dependently-typed setting, we would express this as an inductive proposition or large elimination. We cannot do this in Haskell, but we can at least write an ordinary function that expresses the same basic idea.

lc :: Term a -> Bool
lc = \t -> cata (flip go) t 0 where
  go j = \case
    BVarF i -> i < j
    FVarF _ -> True
    AbsF k -> k (j + 1)
    AppF k1 k2 -> k1 j && k2 j

locally nameless

Table of Contents

1. example implementation in Haskell