Combinatory logic

Datatypes

Continuation passing for linear datatypes

Direct product

• $\Diamond _{2}\equiv \lambda \;x\;y\;f\;.\;f\;x\;y$

in $lambda$-calculus and

• $\Diamond _{2}\equiv \;\mathbf {C_{1}} \;\mathbf {C_{*}}$

in combinatory logic.

A nice generalization scheme:

• as the $\langle \dots \rangle$ construct can be generalized to any natural number $n$ (the concept of $n$-tuple, see Barendregt's $\lambda$ Calculus)
• and in this generalizedscheme $\mathbf {I}$ corresponds to the 0 case, $\mathbf {C_{*}}$ to the 1 case, and the ordered pair construct $\Diamond _{2}$ to the 2 case, as though defining
  • $\Diamond _{0}\equiv \mathbf {I}$
  • $\Diamond _{1}\equiv \mathbf {C_{*}}$

so we can write definition

• $\Diamond _{2}\equiv \mathbf {C_{1}} \;\mathbf {C_{*}}$

or the same

• $\Diamond _{2}\equiv \mathbf {C} \cdot \mathbf {C_{*}}$

in a more interesting way:

• $\Diamond _{2}\equiv \mathbf {C} \cdot \Diamond _{1}$

Is this generalizable? I do not know. I know an analogy in the case of left, right, just, nothing.

We know this construct well when defining operations for booelans, and church-numbers. But in generally, in defining datatypes in this continuation-passing way, then operations on so-defined datatypes often turn to be well-definable by $\Diamond _{2}$

Catamorphisms for recursive datatypes

List

Let us define the concept of list by its catamorphism (see Haskell's foldr): a list (each concrete list) is a function taking two arguments

• a two-parameter function argument (cons-continuation)
• a zero-parameter function argument (nil-continuation)

and returns a value coming from a term consisting of applying cons-continuations and nil-continuations in the same shape as the correspondig list. E. g. in case of having defined

• $\mathrm {oneTwoThree} \equiv \mathrm {cons} \;1\;\left(\mathrm {cons} \;2\;\left(\mathrm {cons} \;3\;\mathrm {nil} \right)\right)$

the expression

• $\mathrm {oneTwoThrhree} +0$

reduces to

• + 1 (+ 2 (+ 3 0))

But how to define cons and nil? In $\lambda$-calculus

• $\mathrm {nil} \equiv \lambda \;c\;n\;.\;n$
• $\mathrm {cons} \equiv \lambda \;h\;t\;c\;n\;.\;c\;h\;\left(t\;c\;n\right)$

does the job. Let us think of the variables as $h$ denoting head, $t$ denoting tail, $c$ denoting cons-continuation, and $n$ denoting list-continuation.

Using the formulating combinators described in CUrry: Combinatory Logic I, we can traslate these definitions into combinatory logic without any pain:

• $\mathrm {nil} \equiv \mathbf {K} _{*}$
• $\mathrm {cons} \equiv \mathbf {B} \left(\mathbf {\Phi } \;\mathbf {B} \right)\mathbf {C_{*}}$

Of course we could use the two parameters in the opposite order, but I am not sure yet that it would provide a more easy way.

A little practice: let us define concat. In Haskell, we ca do that by

concat = foldr (++) []

which corresponds in cominatory logic to reducing

• $\mathrm {concat} \;l\equiv l\;\mathrm {append} \;\mathrm {nil}$

Let us use the ordered pair (direct product) construct:

• $\mathrm {concat} \equiv \Diamond _{2}\;\mathrm {append} \;\mathrm {nil}$

and if I use that nasty centred (see later)

• $\mathrm {concat} \equiv \mathrm {centred} \;\mathrm {append}$

Monads in Combinatory Logic?

Concrete monads

The list as a monad

We could name

• \mathrm{concat} \equiv \mathrm{list\!\!-\!\!join}

Now let us see mapping a list, concatenating a list, binding a list. Mapping and binding have a common property: yielding nil for nil. I shall say these operations are centred: their definition would contain a $\mathbf {C} \;\Diamond _{2}\;\mathrm {nil}$ subexpression. Thus I shall give a name to this subexpression:

• $\mathrm {centred} \equiv \mathbf {C} \;\Diamond _{2}\;\mathrm {nil}$

Now let us define map and bind for lists:

• $\mathrm {list\!\!-\!\!map} \equiv \mathrm {centred} _{1}\;\mathrm {cons} _{1}$
• $\mathrm {list\!\!-\!\!=\!\!<\!\!<} \equiv \mathrm {centred} _{1}\;\mathrm {append} _{1}$

now we see it was worth of defining a common $\mathrm {centred}$. But to tell the truth, it may be a trap. centred breaks a symmetry: we should always define the cons and nil part of the foldr construct on the same level, always together. Modularization should be pointed towards this direction, and not to run forward into the T-street of centred.

Another remark: of course we can get the monadic bind for lists

• $\mathrm {list\!\!-\!\!>\!\!>\!\!=} \equiv \mathbf {C} \;\mathrm {list\!\!-\!\!=\!\!<\!\!<}$

But we used append here. How do we define it? It is surprizingly simple. Let us think how we would define it in Haskell by foldr, if it was not defined already as ++ defined in Prelude: In defining

(++) list1 list2

we can do it by foldr:

(++) [] list2 = list2
(++) (a : as) list2 = a : (++) as list2

thus

(++) list1 list2 = foldr (:) list2 list1

let us se how we should reduce its corresponding expression in Combinatory Logic:

• $\mathbf {append} \;l\;m\to l\;\mathbf {cons} \;m$

thus

• $\mathbf {append} \,l\,m=l\,\mathbf {cons} \,m$
• $\mathbf {append} \;l=\!\!_{1}\;l\;\mathbf {cons}$
• $\mathbf {append} \equiv \mathbf {C_{*}} \;\mathbf {cons}$

Thus, we have defined monadic bind for lists. I shall call this the deforested bind for lists. Of course, we could define it another way too: by concat and map, which corresponds to defining monadic bind from monadic map and monadic join. But I think this way forces my CL-interpreter to manage temporary lists, so I gave rather the deforested definition.

Defining the other monadic operation: return for lists is easy:

instance Monad [] where
        return = (: [])

in Haskell -- we know,

(: [])

translates to

return = flip (:) []

so

• $\mathrm {list\!\!-\!\!return} \equiv \mathbf {C} \;\mathrm {cons} \;\mathrm {nil}$

How to AOP with monads in Combinatory Logic?

We have defined monadic list in CL. Of course we can make monadic Maybe, binary tree, Error monad with direct sum constructs...

But separation of concerns by monads is more than having a bunch of special monads. It requires other possibilities too: e.g. being able to use monads generally, which can become any concrete mondads.

Of course my simple CL interpreter does not know anything on type classes, overloading. But there is a rather restricted andstatic possibility provided by the concept of definition itself:

• $\mathrm {work} \equiv \mathrm {A\!\!-\!\!>\!\!>\!\!>\!\!=} \;\mathrm {subwork\!\!-\!\!1} \;\mathrm {parametrized\!\!-\!\!subwork\!\!-\!\!2}$

and later we can change the binding mode named A e.g. from a failure-handling Maybe-like one to a more general indeterminism-handling list-like one, then we can do that simply by replacing definition

• $\mathrm {A\!\!-\!\!>\!\!>\!\!>\!\!=} \equiv \mathrm {maybe\!\!-\!\!>\!\!>\!\!>\!\!=}$

with definition

• $\mathrm {A\!\!-\!\!>\!\!>\!\!>\!\!=} \equiv \mathrm {list\!\!-\!\!>\!\!>\!\!>\!\!=}$