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...
