haskellpointfreetacit-programming

How to rewrite in point-free style with a repeating variable?

How to rewrite the following expression in point-free style?

p x y = x*x + y

Using the lambda-calculus I did the following:

p = \x -> \y -> (+) ((*) x x) y
  = \x -> (+) ((*) x x) -- here start my problem
  = \x -> ((+) . ((*) x )) x
  ... ?
Solution

  • Since you mentioned Lambda Calculus I will suggest how to solve this with SK combinators. η-reduction was a good try, but as you can tell you can't η-reduce when the variable is used twice.

    S = λfgx.fx(gx)
K = λxy.x

    The feature of duplication is encoded by S. You simplified your problem to:

    λx.(+)((*)xx)

    So let us start there. Any lambda term can be algorithmically transformed to a SK term.

    T[λx.(+)((*)xx)]
= S(T[λx.(+)])(T[λx.(*)xx])        -- rule 6
= S(K(T[(+)]))(T[λx.(*)xx])        -- rule 3
= S(K(+))(T[λx.(*)xx])             -- rule 1
= S(K(+))(S(T[λx.(*)x])(T[λx.x]))  -- rule 6
= S(K(+))(S(*)(T[λx.x]))           -- η-reduce
= S(K(+))(S(*)I)                   -- rule 4

    In Haskell, S = (<*>) and K = pure and I = id. Therefore:

    = (<*>)(pure(+))((<*>)(*)id)

    And rewriting:

    = pure (+) <*> ((*) <*> id)

    Then we can apply other definitions we know:

    = fmap (+) ((*) <*> id)     -- pure f <*> x = fmap f x
= fmap (+) (join (*))       -- (<*> id) = join for Monad ((->)a)
= (+) . join (*)            -- fmap = (.) for Functor ((->)a)