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... _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe