This message is a literate Haskell98 code for translating proper linear combinators into a point-free style. That is, we will be converting (closed, albeit that is not strictly a requirement) terms of the form ``\x1 ... xn -> term'' where each variable xi has at most one occurrence in term. The technique can be easily generalized to non-linear terms. Other possible generalizations is automatical derivation of the point-less code from the _signature_ of a function. The body of the function isn't actually needed, for applicative and tuple fully-polymorphic functions.

module PF where

Our terms have the following simple structure

data Term = Var String | CId -- identity | CC -- composition | CK -- const | CF -- flip | A Term Term deriving (Eq, Show)

and a bit of standard term-rewriting grind

occurs v v' | v == v' = True occurs v (A t1 t2) = occurs v t1 || occurs v t2 occurs _ _ = False

ground (Var _) = False ground (A t1 t2) = ground t1 && ground t2 ground _ = True

We introduce term normalization. A normalized term has the following structure data NT = Ground | A NT Var | A NT Ground that is, the term tree is linear with respect to variables. After normalization, our (closed) source term \x1 ... xn -> term becomes \x1 ... xn -> term' y1 ... ym where each y1 is either a variable or a ground term, and term' is ground. Furthermore, if we drop ground terms from the list y1 ... ym, it becomes a permutation of a subset of x1 ... xn. The normalization is easily performed by tree rotations

norm t | ground t = t norm (A t1 v@(Var _)) = A (norm t1) v norm (A t1 t2) | ground t2 = A (norm t1) t2 norm (A t1 (A t2 t3)) = norm (A (A (A CC t1) t2) t3) norm v@(Var _) = A CId v norm c = c

As you can see, guards are prominent. A few tests

test1 = norm (A (Var "f") (A (A (Var "g") (Var "a")) (Var "b")))

-- \f g h x y -> f (g x) (h y) test2 = norm (A (A (Var "f") (A (Var "g") (Var "x"))) (A (Var "h") (Var "y")))

test32 = norm (A CF (A (A (A (A CId CC) CC) (Var "f")) (Var "g"))) test34 = norm (A (A CC (A CC CF)) (A (A CId CC) CC)) test35 = norm (A (A CC (A (Var "g") CF)) (A (A CId CC) CC))

The next step is elimination of variables using eta-reductions, const introductions, and flips to bring the variables into the right position. The function `elim' takes a list of free variables to eliminate, in reverse order, and the term. The function returns the point-free term.

elim [] t = t -- eta reduction, linearity assumption elim (h:r) (A t v) | h == v = elim r t -- if \a b -> t a b then -- \a b x -> const (t a b) x elim (h:r) t | not (occurs h t) = elim r (norm (A CK t)) elim v@(h:r) t = elim v (norm (doflip h t)) where doflip v (A (A t v1) v2) | v == v1 = (A (A (A CF t) v2) v1) doflip v (A t v2) = A (doflip v t) v2 doflip v t = error $ (show v) ++ "\n" ++ (show t)

And that is it. We just need to print the terms nicely:

print_nice (Var v) = show v print_nice (A (A CC x) y) = "(" ++ (print_nice x) ++ " . " ++ (print_nice y) ++ ")" print_nice (A CC x) = "(" ++ (print_nice x) ++ " .)" print_nice (A x y) = "(" ++ print_nice x ++ ") (" ++ print_nice y ++ ")" print_nice CC = "(.)" print_nice CK = "const" print_nice CId = "id" print_nice CF = "flip"

report' vars term = elim (reverse $ (map Var) vars) (norm term) report vars = print_nice . report' vars

We are ready for some tests: The first two tests are trivial: \f x y -> f x y

test11 = report ["f","x","y"] (A (A (Var "f") (Var "x")) (Var "y"))

*PF> test11 "id" And \f x y -> f y x

test12 = report ["f","x","y"] (A (A (Var "f") (Var "y")) (Var "x"))

*PF> test12 "(flip . id)" the next one is simple too: \f x y -> f x

test13 = report ["f","x","y"] (A (Var "f") (Var "x"))

*PF> test13 "((const .) . id)" Now we can try \f g a b -> f (g a b)

test14 = report ["f","g","a","b"] (A (Var "f") (A (A (Var "g") (Var "a")) (Var "b")))

*PF> test14 "((.) . (.))" and \f g h x y -> f (g x) (h y)

test15 = report ["f","g","h","x","y"] (A (A (Var "f") (A (Var "g") (Var "x"))) (A (Var "h") (Var "y")))

*PF> test15 "((flip .) . ((.) . ((.) .)))" The reported derivation was ((flip . ((.) .)) .) . (.) These terms are equivalent. One may look at their types, which are identical. One may also apply these terms to suitable arguments, e.g., ((flip .) . ((.) . ((.) .))) (,) ((,) 1) ((,) 2) 3 4 This sub-thread started from \f g a b -> f (g a b): two-to-one composition, aka triple-(.). Can we generalize? Certainly: \f g a b c -> f (g a b c)

test16 = report ["f","g","a","b","c"] (A (Var "f") (A (A (A (Var "g") (Var "a")) (Var "b")) (Var "c")))

*PF> test16 "(((.) . (.)) . (.))" \f g a b c d -> f (g a b c d)

test17 = report ["f","g","a","b","c","d"] (A (Var "f") (A (A (A (A (Var "g") (Var "a")) (Var "b")) (Var "c")) (Var "d")))

*PF> test17 "((((.) . (.)) . (.)) . (.))" *PF> ((((.) . (.)) . (.)) . (.)) ((,) 1) (,,,) 10 11 12 13 (1,(10,11,12,13)) \f g h a b c d -> f (g a b) (h c d)

test18 = report ["f","g","h","a","b","c","d"] (A (A (Var "f") (A (A (Var "g") (Var "a")) (Var "b"))) (A (A (Var "h") (Var "c")) (Var "d")))

*PF> test18 "((flip .) . (((flip .) .) . (((.) . (.)) . (((.) . (.)) .))))" It really begins to look like Unlambda...