What Happens to Currying When Beta and Eta Become Computations?

Fix a type $O$, a closed function $f:O\Rightarrow O$, and one free input $y:O$. Consider the term

It contains two beta redexes. We can contract the outer one first,

or the inner one first,

Ordinary beta equality tells us that $T(y)=f\,y$. That statement is correct, but it does not tell us that two contractions occurred, or that they can occur in either order.

Robert Seely's 1987 paper Modelling Computations: A 2-Categorical Framework asks what happens when we refuse to erase that information. His answer changes the usual roles of beta and eta. They stop being equations that justify a cartesian closed structure and become directed cells that build a two-dimensional version of it.

After reading this article, you should be able to use the term $T$ to explain four points:

1. why a conversion is naturally a 2-cell;
2. why substitution forces some reduction histories to be identified;
3. why eta and beta become the unit and counit of an adjunction between currying and uncurrying;
4. why $E\Rightarrow-$ preserves composition through a beta comparison rather than by equality.

The intended reader knows typed lambda calculus, substitution, beta and eta, and the ordinary idea of currying. Some basic category theory is helpful, but the category-theoretic notation needed for the central calculation is explained as it appears. No domain theory or 2-category theory is assumed.

1. What does equality forget?Copy link to section

Start with the smaller redex

In the usual equational theory, we quotient terms by beta conversion. The two expressions then represent the same term. In a cartesian closed category, they are interpreted by the same morphism.

This is useful when the question is extensional: do the programs have the same result? It is insufficient when the reduction itself matters. Equality retains the endpoints and discards the witness between them.

Seely's first move is simple. Keep the typed terms as arrows, but place a new kind of arrow between parallel terms:

The symbol $p$ is not another program. It is the beta conversion from one program expression to another. This gives three levels of structure:

The direction $B\to A$ says that the term consumes one free input of type $B$ and produces a result of type $A$. If a term has several free variables, Seely packages their context into a product. The one-input presentation therefore does not restrict the programs we can describe.

The mental model is now this: types are boundaries, terms are programs between those boundaries, and conversions are computations between programs.

2. Why are reduction arrows alone not enough?Copy link to section

Once conversions are kept, they must compose in two ways.

Chaining steps gives vertical compositionCopy link to section

The first composition is familiar. If

then we can run $p$ followed by $q$:

Each of the two routes from $T(y)$ to $f\,y$ is a vertical composite of two beta conversions. The target of the first step must match the source of the second.

Placing a step in a context gives horizontal compositionCopy link to section

The second composition comes from substitution. Return to the two open terms

and their beta conversion $p:a\Rightarrow b$. Now define

with the inner conversion $r:d\Rightarrow e$.

Substituting $d(y)$ for $x$ in $a(x)$ produces the running term:

The conversion $r$ can also be placed inside the context $(\lambda u.u)[-]$:

This is substitution acting on a computation. In 2-category language it is a special case of horizontal composition. In general, from

substitution constructs

The important point is computational: a valid local conversion remains valid when a larger term uses it.

3. Why must the two paths be identified?Copy link to section

We can now label every step in the two reductions of $T$.

The outer-first route is

The inner-first route is

Both routes start at $T(y)$ and end at $f\,y$. More is true: each route applies the same outer conversion and the same substituted conversion, only in the opposite order.

Here $p[d/x]$ means that the term $d$ is substituted into both the source and target of the cell $p$. The notation $a[r]$ means that the cell $r$ is placed inside the term context $a[-]$; $b[r]$ and $p[e/x]$ are read in the same way. The four labels therefore name ordinary substitution operations, now applied to conversions as well as terms.

Figure 1. Interchange identifies the outer-first and inner-first routes. The figure answers which scheduling distinction Seely's strict 2-category chooses not to retain.

For composition of terms to act functorially on conversions, the square must commute. Seely therefore imposes the equation

This is the interchange law in the concrete language of substitution. The common 2-cell is the horizontal composite $p*r$.

A common misconception: 2-cells are raw execution tracesCopy link to section

They are not raw traces in Seely's construction. The two sequences above look different as schedules, but the 2-category identifies them. More equations are added later for naturality and coherence.

Seely's model therefore sits between two extremes:

• ordinary equational semantics erases every conversion between equal terms;
• a raw trace model distinguishes every sequence of steps;
• LAMBDA keeps directed conversions, then quotients some sequences so that substitution is compositional.

That middle position is the main conceptual obstacle in the paper. Replacing an equality by an arrow is only the beginning. One must also decide which arrows count as the same computation.

4. What structure have we built?Copy link to section

Seely calls the resulting 2-category LAMBDA. Starting from primitive types, its types are closed under products and function types:

Its terms use pairing, projections, lambda abstraction, and application. The function-type conversions are directed:

The eta rule may look reversed. Many presentations use eta contraction, $\lambda x.c(x)\Rightarrow c$. Seely initially chooses eta expansion because the direction will supply the unit of the adjunction in Section 5.

The rest of the construction is compact:

• objects are types;
• 1-cells are one-input typed terms;
• 2-cells are directed conversions modulo the equations needed for the 2-category laws;
• 1-cell composition is substitution;
• vertical composition chains conversions;
• horizontal composition substitutes conversions.

One technical convention will matter below. Seely treats alpha conversion as identity, and he collapses the product beta and eta conversions to identities so that the paper can concentrate on function types. Associativity of 1-cell composition is inherited from typed substitution. The construction therefore does not promote every lambda-calculus equation to a nontrivial 2-cell.

5. What becomes of currying?Copy link to section

The endpoint of our running example was $f\,y$. Categorically, application is described by evaluation. At the types already fixed in the example, write

with

Currying evaluation turns the stored function into a lambda abstraction:

Uncurrying it again recreates an application, and therefore a beta redex:

The original endpoint has now reappeared for a structural reason: currying introduces the abstraction $\lambda z.fz$, and uncurrying exposes the beta step that removes it.

In an ordinary cartesian closed category, product with $O$ is left adjoint to function space out of $O$. Here $\mathcal C(X,Y)$ means the set of arrows from $X$ to $Y$. Saying that the two constructions are adjoint means, at this ordinary one-dimensional level, that currying gives a natural bijection

When beta and eta are equations, currying and uncurrying are inverse maps. In LAMBDA, the arrows from one type to another form a hom-category: terms are its objects, and conversions between parallel terms are its morphisms. Currying and uncurrying now give functors between these hom-categories.

Call currying $K$ and uncurrying $L$:

Let $d:A\mathbin{\&}O\to B$. Currying isolates the $O$ input:

Let $c:A\to(O\Rightarrow B)$. Uncurrying applies the function stored at the first projection to the argument stored at the second:

Now we can derive one composite line by line:

Thus beta supplies a conversion

For the other composite, unfold the definitions again:

Seely's eta orientation points from $c(x)$ to this expanded term:

So eta supplies candidate cells $1\Rightarrow KL$, while beta supplies $LK\Rightarrow 1$. The two calculations alone do not yet prove an adjunction. The cells must be natural in the terms they transform, and both triangle identities must hold. Seely's naturality and coherence equations establish those facts. With those equations in place, eta and beta are the unit and counit of

This is the payoff. Currying and uncurrying are no longer inverse functions between hom-sets. They are adjoint functors between hom-categories, and the computations that used to disappear into equality now witness the adjunction.

One of the triangle calculations has a direct computational reading. At evaluation, eta followed by beta gives

Seely imposes that this matching eta-beta operation acts as the identity conversion, and the corresponding coherence equation handles the other triangle. The raw two-step history does not become an identity by endpoint equality alone.

6. Where does laxity enter?Copy link to section

The adjunction above varies with its types. To understand why that variation is not strict, reuse the type $O$ from the running example and consider the function-space constructor

Suppose $m:B\to A$. The induced map

takes a function $g:O\Rightarrow B$ and postcomposes it with $m$:

Now let $n:C\to B$ and start with $g:O\Rightarrow C$. Applying $G(n)$ and then $G(m)$ creates a beta redex that the direct composite does not contain:

Check the types at the middle line. The term $gz$ has type $C$, so $n(gz)$ has type $B$, and $m(n(gz))$ has type $A$. Abstracting over $z:O$ therefore gives a term of type $O\Rightarrow A$ on both sides.

The beta conversion above is the comparison 2-cell

The identity comparison is the same eta expansion seen in the currying calculation. For $q:O\Rightarrow A$:

This is what lax means here. It does not mean approximate or defective. Composition and identity are preserved through specified directed 2-cells rather than literal equalities.

This calculation exhibits the two comparison cells; it is not the whole lax functor proof. The constructor must also act on conversions, and the comparison cells must satisfy naturality, associativity, and identity coherence. Seely checks those remaining laws in the construction of LAMBDA.

Under Seely's treatment of products, $F=-\mathbin{\&}O$ is strict, while $G=O\Rightarrow-$ is lax. The families $K_{A,B}$ and $L_{A,B}$ are strict in their first type argument and lax in their second. Seely packages the comparison cells, unit, and counit into what he calls a lax semantic adjunction. This is his specific 1987 notion, so it should not be renamed a strict modern 2-adjunction.

7. Can the two paths be represented in code?Copy link to section

Haskell is useful for a small companion because algebraic data types mirror terms, individual cells, and paths. The program below builds the two reductions of $T$. It checks only their boundaries. It is not a type checker, a beta validator, or an implementation of Seely's quotient.

module Main (main) where
 
data Term
  = Var String
  | Const String
  | Lam String Term
  | App Term Term
  deriving (Eq)
 
instance Show Term where
  show (Var x) = x
  show (Const c) = c
  show (Lam x body) = "(λ" ++ x ++ "." ++ show body ++ ")"
  show (App fun arg) = "(" ++ show fun ++ " " ++ show arg ++ ")"
 
data Rule
  = Beta
  | Inside String Rule
  deriving (Eq, Show)
 
data Step = Step
  { source :: Term
  , target :: Term
  , rule :: Rule
  }
  deriving (Eq, Show)
 
type Path = [Step]
 
startOf :: Path -> Maybe Term
startOf [] = Nothing
startOf (step : _) = Just (source step)
 
endOf :: Path -> Maybe Term
endOf [] = Nothing
endOf steps = Just (target (last steps))
 
valid :: Path -> Bool
valid [] = True
valid [_] = True
valid (first : second : rest) =
  target first == source second && valid (second : rest)
 
liftStep :: String -> (Term -> Term) -> Step -> Step
liftStep context wrap step =
  Step
    (wrap (source step))
    (wrap (target step))
    (Inside context (rule step))
 
sameBoundary :: Path -> Path -> Bool
sameBoundary first second =
  case (startOf first, endOf first, startOf second, endOf second) of
    (Just a, Just b, Just c, Just d) -> a == c && b == d
    _ -> False
 
main :: IO ()
main = do
  let f = Const "f"
      y = Var "y"
      value = App f y
      inner = App (Lam "v" (Var "v")) value
      whole = App (Lam "u" (Var "u")) inner
 
      innerBeta = Step inner value Beta
      outerFirstStep = Step whole inner Beta
      outerAfterInner = Step (App (Lam "u" (Var "u")) value) value Beta
 
      outerFirst =
        [ outerFirstStep
        , innerBeta
        ]
 
      innerFirst =
        [ liftStep "argument of the outer application"
            (App (Lam "u" (Var "u"))) innerBeta
        , outerAfterInner
        ]
 
  print (valid outerFirst, valid innerFirst)
  print (sameBoundary outerFirst innerFirst)

The program prints

(True,True)
True

valid checks that the steps in a path can be composed vertically by comparing adjacent boundaries. liftStep models the action of a term context on a conversion, which is the computational idea behind horizontal composition. sameBoundary confirms that the two paths are parallel.

Parallel paths are not automatically equal. It would be wrong to identify every pair of paths with the same endpoints. Seely's interchange equation justifies identifying this particular pair because it performs the same outer and substituted conversions in opposite orders.

8. What does the construction preserve, and where does it stop?Copy link to section

The 2-category preserves more computational information than an equational model, but less than an operational trace semantics.

It does not preserve every scheduling choiceCopy link to section

Interchange already identified the two reductions of $T$. In the appendix, Seely also requires beta conversions at different logical occurrences to commute. He remarks that this is computationally questionable because an operational model may care about their order.

The construction retains conversion cells modulo specified equations. It does not by itself record cost, evaluation strategy, concurrency, or every intermediate schedule.

The direction of eta is structuralCopy link to section

The unit in the hom-category adjunction points as

If eta is reversed,

the same unit points the wrong way. Section 4 of the paper develops a different and less regular construction, called a lax syntactic adjunction, for that orientation. Changing a rewrite direction changes the categorical property available from it.

Optional background: where the directions come fromCopy link to section

Seely reaches directed beta and eta through models of the untyped lambda calculus. Such a model has a domain $D$ and maps

The map $h$ reads an element as a function, and $k$ encodes a function as an element. Replacing inverse equations by

makes $h$ left adjoint to $k$ in an ordered setting. One inequality gives eta expansion and the other beta contraction. A partial order is a thin category, so Seely's move from inequalities to general hom-categories replaces one possible comparison by a possibly non-thin category of conversions.

This background explains the chosen directions, but it is not needed to follow the worked term or the currying calculation.

Optional extension: polymorphismCopy link to section

For second-order polymorphism, types also contain $\forall t.A$. Seely organizes the resulting terms and conversions into an indexed 2-category called POLYLAMBDA. If $W$ adds an unused type variable, the sketched lax adjunction is

Universal quantification is the lax right adjoint. The paper presents this final section as a mathematical sketch rather than a full development.

9. What mental model should remain?Copy link to section

The transferable idea is not simply that lambda calculus forms a 2-category. It is a sequence of consequences.

Equality remembers that two terms coincide but forgets the conversion between them. Keeping conversions makes them 2-cells. Because a computation must remain valid when substituted into a larger term, those cells compose both vertically and horizontally. Interchange makes the two compositions compatible, at the price of identifying some raw reduction orders.

Once beta and eta are directed cells, currying and uncurrying cannot remain strict inverses. Eta becomes the unit, beta becomes the counit, and the function-space constructor preserves composition through beta comparison cells. That is why laxity appears.

When an equation in a semantic model hides a process, Seely's paper suggests a useful question: can the equation be lifted to a directed cell, and which coherence equations must then be imposed so that the process remains compositional?

Sources and further readingCopy link to section

• R. A. G. Seely, Modelling Computations: A 2-Categorical Framework, LICS 1987, pp. 65-71.
• LICS bibliographic entry and abstract.
• R. A. G. Seely, publication list and related papers.