Designing a Module for Combinatory Logic in Haskell
Like the Lambda Calculus (on which Lisp is based), Combinatory Logic is a formal system that can be used to model and study computation. What makes it fascinating is that it is as powerful as the (already simple) lambda calculus, but has no need for the variables that LC requires to perform substitution!
Here I show how we can use Haskell’s type classes and other language features to model the Combinator Calculus. The goals of this module were:
-
don’t force any one evaluation strategy
-
allow users to define new combinators without exposing the implementation
-
allow new combinators to be defined in terms of other already-defined combinators.
-
discourage creation of non-sensical combinator expressions, or possible mis-use of the module
-
hide existential types and anything else exotic
If you want to play with it, you can do a:
$ git clone https://github.com/jberryman/combinator-calculus.git
A Quick Combinator Calculus Primer
A Combinatory Logic expression consists of a sequence of combinator terms and sub-expressions. Combinator terms are like functions which consume some arguments (themselves combinators or sub-expressions), and return a particular re-arrangement of those arguments. When no term can consume enough arguments to be “evaluated” any further, the expression is said to be in normal form.
The SKI Combinator Calculus is a system
that uses only three combinators (‘S’, ‘K’ and ‘I’) and forms a Turing
Complete system. This means we can express any computation with expressions
that look like SK(SSS)I(S(KS)K)I
. It can even server as the basis of a
turing complete
programming language!
It’s a really fascinating topic, and you can get a great overview from wikipedia’s excellent Combinatory Logic article.
The Design of the Module
All terms in combinatory logic take some arguments and form a new expression from them, but different combinators transform their arguments in different ways.
We can express this in Haskell by creating a typeclass with methods that describe the behavior of a combinator. Then we can make a type (corresponding to a specific Combinator term) an instance of our class to define its behavior.
The Combinator
Class
Here is how we define our Combinator
class:
-- a Class for combinators. Its methods represent a combinator's behavior on
-- its arguments:
class (Show c)=> Combinator c where
takesArgs :: c -> Int
applyArgs :: c -> [Term] -> Expr
-- HIDDEN METHOD: EXPORTED AS A FUNCTION:
-- if a combinator takes 0 args, we assume it can be evaluated and we
-- say it is not in Normal Form:
isNormal :: c -> Bool
isNormal = (> 0) . takesArgs
-- HIDDEN METHOD: user defined combinators are placed in a black box:
toTerm :: c -> Term
toTerm = Term
The first two methods are the only ones exported to users of the module to
define an instance of Combinator
. takesArgs
is used to indicate how many
arguments this particular combinator requires before it can be evaluated.
applyArgs
actually performs the transformation of those arguments; it is
given a list of terms (of length equal to takesArgs
) and returns a new
expression (type Expr).
The third method is used to check if an expression is in normal form. It is exported as a regular function, meaning that users can use it in their code but cannot use it in their own instance declarations. Instead the default value would apply.
The fourth method toTerm
is used internally to encapsulate some Combinator
class item in a Term
data type. We use this when composing combinator
expressions, in order to preserve the tree structure of the expression. (see
below for more on this)
The Term
and Expr
types
The module defines two new datatypes, both of which are instances of
Combinator
.
Expr
is a newtype
wrapper around Seq Term
, but we don’t export the
implementation so we can change this if we don’t want to use
Sequences:
newtype Expr = Expr { combSeq :: Seq Term }
It simply represents a CL expression as a sequence of terms. Making it an
instance of Combinator
expresses the notion that an expression can be
thought of as a combinator term whenever the need arises. In fact the
distinction is simply one of
evaluation strategy.
Term
is a wrapper for Combinator terms and sub-expressions. It is mutually-
recursive with Expr
and the two together form the tree structure of a
combinator expression:
data Term = forall c. Combinator c => Term { unbox :: c }
| SubExpr { subExpr :: Expr }
| NamedExpr { subExpr :: Expr,
name :: String }
All three constructors are hidden from the user. SubExpr
simply holds an
Expr
type and represents a parenthesized sub-expression within the top level
combinator sequence. NamedExpr
is identical except that it also contains a
String, which will be returned when show
is called on that constructor. Here
is the Show
instance for Term
:
instance Show Term where
show (NamedExpr _ n) = n
show (SubExpr e) = "("++ show e ++")"
show (Term t) = show t
The remaining constructor is the most interesting: the Term
constructor
houses an
existentially-quantified type and
can hold any type value of the Combinator
class.
Notice that the type variable does not appear on the left side of the =
in
the type declaration. What this means in practical terms is that the Term
constructor becomes a “black box”; once a value is inside, the only things we
can “do with it” are to apply polymorphic Combinator class functions and
methods.
And that’s why we have the internal toTerm
method; it allows us to wrap sub-
expressions in the SubExpr
constructor, preserving the tree structure of an
expression as we compose it. Without it we would either need to export
multiple functions for composing a term with an expression, an expression with
an expression, a term with a term, and an expression with a term. Ugly!
Exported functions
Our types and classes allow us to do some neat stuff. As mentioned above, we can compose expressions using a single haskell infix function. Since all the nice ASCII combinators were taken (and since I’m the only one using this) I decided to go with a Unicode symbol, the middle dot, for composition:
-- operator for composing combinator expressions. This is the Middle Dot,
-- unicode character 00B7. It is easily inserted in vim using the digraph:
-- Ctrl-K '.' 'M'
infixl 7 ·
…and the implementation:
-- for composing Combinator expressions:
(·) :: (Combinator c1,Combinator c2)=> c1 -> c2 -> Expr
c1 · (toTerm->t2) =
case toTerm c1 of
(SubExpr e) -> e `appendTerms` singleton t2
-- named expression or bare Term start a new sub-expression:
t1 -> Expr (singleton t1 |> t2)
We also have the ability to define new combinators in terms of other
combinators using the named
function. Here is an example showing how I
can
be defined in terms of S
and K
and used to form a Combinator Calculus
equivalent of the
Church Numeral 2:
two = S·(S·(K·S)·K)·cI
where cI = (S · K · K) `named` "I"
Playing with it
The evaluation function exported in the module was written fairly hastily, but it is good enough to let us play with evaluating expressions.
I’ve run out of time on this post, but you can grab the darcs repo above and
run the ‘main’ function in Examples.hs
and check out the source for more
info. I’ll maybe show some cool examples in a later post.
Thanks for reading!