[Haskell-cafe] Automatic pointless translation

[oleg at pobox.com]

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