Revision as of 14:28, 3 March 2006

Portals and other large-scale resources

Implementing CL

Talks about it at haskell-cafe $\subset$ haskell-cafe
Lot of interpreters at John's Lambda Calculus and Combinatory Logic Playground
CL++, a lazy-evaluating combinatory logic interpreter with some computer algebra service: e.g. it can reply the question $+ 2 3;$ with $5$ instead of a huge amount of parantheses and $K$ , $S$ combinators. Unfortunately I have not written it directly in English, so all documantations, source code and libraries are in Hungarian. I want to rewrite it using more advanced Haskell programming concepts (e.g. monads or attribute grammars) and directly in English.

Programming in CL

I think many thoughts from John Hughes' Why Functional Programming Matters can be applied to programming in Combinatory Logic. And almost all concepts used in the Haskell world (catamorphisms etc.) helps us a lot here too. Combinatory logic is a powerful and concise programming language. I wonder how functional logic programming could be done by using the concepts of Illative combinatory logic, too.

Datatypes

Continuation passing for polynomial datatypes

Direct product

Let us begin with a notion of the ordered pair and denote it by $◊_{2}$ . We know this construct well when defining operations for booleans

$t r u e \equiv K$
$f a l s e \equiv K_{*}$
$n o t \equiv ◊_{2} f a l s e t r u e$

and Church numbers. I think, in generally, when defining datatypes in a continuation-passing way (e.g. Maybe or direct sum), then operations on so-defined datatypes often turn to be well-definable by some $◊_{n}$ .

We define it with

$◊_{2} \equiv λ x y f . f x y$

in $l a m b d a$ -calculus and

$◊_{2} \equiv C_{(1)} C_{*}$

in combinatory logic.

A nice generalization scheme:

as the $⟨ \dots ⟩$ construct can be generalized to any natural number $n$ (the concept of $n$ -tuple, see Barendregt's $λ$ Calculus)
and in this generalized scheme I corresponds to the 0 case, C* to the 1 case, and the ordered pair construct ◊2 to the 2 case, as though defining
- $◊_{0} \equiv I$
- $◊_{1} \equiv C_{*}$

so we can write definition

$◊_{2} \equiv C_{(1)} C_{*}$

or the same

$◊_{2} \equiv C \cdot C_{*}$

in a more interesting way:

$◊_{2} \equiv C \cdot ◊_{1}$

Is this generalizable? I do not know. I know an analogy in the case of $l e f t$ , $r i g h t$ , $j u s t$ , $n o t h i n g$ .

Direct sum

The notion of ordered pair mentioned above really enables us to deal with direct products. What about it dual concept? How to make direct sums in Combinatory Logic? And after we have implemented it, how can we see that it is really a dual concept of direct product?

A nice argument described in David Madore's Unlambda page gives us a continuation-passig style like solution. We expect reductions like

$l e f t x \to λ f g . f x$
$r i g h t x \to λ f g . g x$

so we define

$l e f t \equiv λ x f g . f x$
$r i g h t \equiv λ x f g . g x$

now we translate it from $λ$ -calculus into combinatory logic:

$l e f t \equiv K_{(2)} C_{*}$
$r i g h t \equiv K_{(1)} C_{*}$

Of course, we can recognize Haskell's Either (Left, Right).

Maybe

Let us remember Haskell's maybe:

maybe :: a' -> (a -> a') -> Maybe a -> a'
maybe n j Nothing = n
maybe n j (Just x) = j x

thinking of

n as nothing-continuation
j as just-continuation

In a continuation passing style approach, if we want to implement something like the Maybe constuct in $λ$ -calculus, then we may expect the following reductions:

$n o t h i n g \equiv λ n j . n$
$j u s t x \to λ n j . j x$

we know both of them well, one is just $K$ , and we remember the other too from the direct sum:

$n o t h i n g \equiv K$
$j u s t \equiv r i g h t$

thus their definition is

$n o t h i n g \equiv K$
$j u s t \equiv K_{(1)} C_{*}$

where both $j u s t$ and $r i g h t$ have a common definition.

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

$o n e T w o T h r e e \equiv c o n s 1 (c o n s 2 (c o n s 3 n i l))$

the expression

$o n e T w o T h r e e + 0$

reduces to

$+ 1 (+ 2 (+ 3 0))$

But how to define $c o n s$ and $n i l$ ? In $λ$ -calculus, we should like to see the following reductions:

$n i l c n \to n$
$c o n s h t \to λ c n . c h (t c n)$

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

Thus, we could achieve this goal with the following definitions:

$n i l \equiv λ c n . n$
$c o n s \equiv λ h t c n . c h (t c n)$

Using the formulating combinators described in Haskell B. Curry's Combinatory Logic I, we can translate these definitions into combinatory logic without any pain:

$n i l \equiv K_{*}$
$c o n s \equiv B (Φ B) 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 can do that by

concat = foldr (++) []

which corresponds in cominatory logic to reducing

$c o n c a t l \equiv l a p p e n d n i l$

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

$c o n c a t \equiv ◊_{2} a p p e n d n i l$

and if I use that nasty $c e n t r e d < / m a t h b f >$ (see later)

$c o n c a t \equiv c e n t r e d a p p e n d$

Monads in Combinatory Logic?

Concrete monads

Maybe as a monad

return

Implementing the return monadic method for the Maybe monad is rather straightforward, both in Haskell and CL:

instance Monad Maybe
        return = Just
        ...

$m a y b e - r e t u r n \equiv j u s t$

map

Haskell:

instance Functor Maybe where
        map f = maybe Nothing (Just . f)

$λ$ -calculus: Expected reductions:

$m a y b e - m a p f p \to p n o t h i n g (j u s t_{(1)} f)$

Definition:

$m a y b e - m a p \equiv λ f p . p n o t h i n g (j u s t_{(1)} f)$

Combinatory logic: we expect the same reduction here too

$m a y b e - m a p f p \to p n o t h i n g (j u s t_{(1)} f)$

let us get rid of one parameter:

$m a y b e - m a p f \to ◊_{2} n o t h i n g (j u s t_{(1)} f)$

now we have the definition:

$m a y b e - m a p \equiv ◊_{2} n o t h i n g \cdot j u s t_{(1)}$

bind

Haskell:

instance Monad Maybe (>>=) where
        (>>=) f p = maybe Nothing f

$λ$ -calculus: we expect

$m a y b e - = < < f p \to p n o t h i n g f$

achieved by defintion

$m a y b e - = < < \equiv λ f p . p n o t h i n g f$

In combinatory logic the above expected reduction

$m a y b e - = < < f p \to p n o t h i n g f$

getting rid of the outest parameter

$m a y b e - = < < f \to ◊_{2} n o t h i n g f$

yielding definition

$m a y b e - = < < \equiv ◊_{2} n o t h i n g$

and of course

$m a y b e - > > = \equiv C m a y b e - = < <$

But the other way (starting with a better chosen parameter order) is much better:

$m a y b e - > > = p f \to p n o t h i n g f$
$m a y b e - > > = p \to p n o t h i n g$

yielding the much simplier and more efficient definition:

$m a y b e - > > = \equiv C_{*} n o t h i n g$

We know already that $C_{*}$ can be seen as as a member of the scheme of tuples: $◊_{n}$ for $n = 1$ case. As the tupe construction is a usual guest at things like this (we shall meet it at list and other maybe-operations like $m a y b e - j o i n$ ), so us express the above definition with $C_{*}$ denoted as $◊_{1}$ :

$m a y b e - > > = \equiv ◊_{1} n o t h i n g$

hoping that this will enable us some interesting generalization in the future.

But why we have not made a more brave genralization, and express monadic bind from monadic join and map? Later in the list monad, we shall see that it may be better to avoid this for sake of deforestation. Here a maybe similar problem will appear: the problem of superfluous $I$ .

join

$m a y b e - j o i n \equiv ◊_{2} n o t h i n g I$

We should think of changing the architecture if we suspect that we could avoid $I$ and solve the problem with a more simple construct.

The list as a monad

Let us think of our list-operations as implementing monadic methods of the list monad. We can express this by definitions too, e.g.

we could name

$l i s t - j o i n \equiv c o n c a t$

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 $C ◊_{2} n i l$ subexpression. Thus I shall give a name to this subexpression:

$c e n t r e d \equiv C ◊_{2} n i l$

Now let us define map and bind for lists:

$l i s t - m a p \equiv {c e n t r e d}_{(1)} {c o n s}_{(1)}$
$l i s t - = < < \equiv {c e n t r e d}_{(1)} {a p p e n d}_{(1)}$

now we see it was worth of defining a common $c e n t r e d$ . But to tell the truth, it may be a trap. $c e n t r e d$ 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 $c e n t r e d$ .

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

$l i s t - > > = \equiv C l i s t - = < <$

But we used $a p p e n d$ 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:

$a p p e n d l m \to l c o n s m$

thus

$a p p e n d l m = l c o n s m$
$a p p e n d l =_{1} l c o n s$
$a p p e n d \equiv C_{*} c o n s$

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

$l i s t - r e t u r n \equiv C c o n s n i l$

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:

$w o r k \equiv A - > > > = s u b w o r k - 1 p a r a m e t r i z e d - s u b w o r k - 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

$A - > > > = \equiv m a y b e - > > > =$

with definition

$A - > > > = \equiv l i s t - > > > =$

Illative Combinatory Logic

Systems of Illative Combinatory Logic complete for first-order propositional and predicate calculus by Henk Barendregt, Martin Bunder, Wil Dekkers.

I think combinator $G$ can be thought of as something analogous to Dependent types: it seems to me that the dependent type construct $\forall x : S \Rightarrow T$ of Epigram corresponds to $G S (λ x . T)$ in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:

$r e a l N u l l v e c t o r : \forall n : N a t \Rightarrow R e a l V e c t o r n$
$G N a t R e a l V e c t o r r e a l N u l l v e c t o r$

My dream is making something in Illative Combinatory Logic. Maybe it could be theroretical base for a functional logic language?

@@ Line 97: / Line 97: @@
 * <math>\mathbf{oneTwoThree} \equiv \mathbf{cons}\;\mathbf1\;\left( \mathbf{cons}\;\mathbf2\;\left(\mathbf{cons}\;\mathbf3\;\mathbf{nil}\right) \right)</math>
 the expression
-* <math>\mathbf{oneTwoThrree}\;\mathbf+\;\mathbf0</math>
+* <math>\mathbf{oneTwoThree}\;\mathbf+\;\mathbf0</math>
 reduces to
-* \mathbf+\;\mathbf1 (\mathbf+\;\mathbf2 (\mathbf+\;\mathbf3\;\mathbf0))
+* <math>\mathbf+\;\mathbf1\;\left(\mathbf+\;\mathbf2\; \left(\mathbf+\;\mathbf3\;\mathbf0\right)\right)</math>
 But how to define <math>\mathbf{cons}</math> and <math>\mathbf{nil}</math>?
 In <math>\lambda</math>-calculus, we should like to see the following reductions: