Rotate the first argument to a function to become nth

Question

Given a function with at least n arguments, I want to rotate the first argument so that it becomes the nth argument. For example (in untyped lambda calculus):

r(λa. a)                   = λa. a
r(λa. λb. a b)             = λb. λa. a b
r(λa. λb. λc. a b c)       = λb. λc. λa. a b c
r(λa. λb. λc. λd. a b c d) = λb. λc. λd. λa. a b c d

And so on.

Can you write r in a generic way? What if you know that n >= 2?

Here's the problem stated in Scala:

trait E
case class Lam(i: E => E) extends E
case class Lit(i: Int) extends E
case class Ap(e: E, e: E) extends E

The rotation should take Lam(a => Lam(b => Lam(c => Ap(Ap(a, b), c)))) and return Lam(b => Lam(c => Lam(a => Ap(Ap(a, b), c)))), for example.

Answer 1

The trick is to tag the "final" value of the functions involved, since to normal haskell, both a -> b and a -> (b->c) are just functions of a single variable. If we do that, though, we can do this.

{-# LANGUAGE TypeFamilies,FlexibleInstances,FlexibleContexts #-}
module Rotate where

data Result a = Result a

class Rotate f where
  type After f
  rotate :: f -> After f

instance Rotate (a -> Result b) where
  type After (a -> Result b) = a -> Result b
  rotate = id

instance Rotate (a -> c) => Rotate (a -> b -> c) where
  type After (a -> b -> c) = b -> After (a -> c)
  rotate = (rotate .) . flip

Then, to see it in action:

f0 :: Result a
f0 = Result undefined

f1 :: Int -> Result a
f1 = const f0

f2 :: Char -> Int -> Result a
f2 = const f1

f3 :: Float -> Char -> Int -> Result a
f3 = const f2

f1' :: Int -> Result a
f1' = rotate f1

f2' :: Int -> Char -> Result a
f2' = rotate f2

f3' :: Char -> Int -> Float -> Result a
f3' = rotate f3

Answer 2

It's probably impossible without violating the ‘legitimacy’ of HOAS, in the sense that the E => E must be used not just for binding in the object language, but for computation in the meta language. That said, here's a solution in Haskell. It abuses a Literal node to drop in a unique ID for later substitution. Enjoy!

import Control.Monad.State

-- HOAS representation
data Expr = Lam (Expr -> Expr)
          | App Expr Expr
          | Lit Integer

-- Rotate transformation
rot :: Expr -> Expr
rot e = case e of
  Lam f -> descend uniqueID (f (Lit uniqueID))
  _ -> e
  where uniqueID = 1 + maxLit e

descend :: Integer -> Expr -> Expr
descend i (Lam f) = Lam $ descend i . f
descend i e = Lam $ \a -> replace i a e

replace :: Integer -> Expr -> Expr -> Expr
replace i e (Lam f) = Lam $ replace i e . f
replace i e (App e1 e2) = App (replace i e e1) (replace i e e2)
replace i e (Lit j)
  | i == j = e
  | otherwise = Lit j

maxLit :: Expr -> Integer
maxLit e = execState (maxLit' e) (-2)
  where maxLit' (Lam f) = maxLit' (f (Lit 0))
        maxLit' (App e1 e2) = maxLit' e1 >> maxLit' e2
        maxLit' (Lit i) = get >>= \k -> when (i > k) (put i)

-- Output
toStr :: Integer -> Expr -> State Integer String
toStr k e = toStr' e
  where toStr' (Lit i)
          | i >= k = return $ 'x':show i -- variable
          | otherwise = return $ show i  -- literal
        toStr' (App e1 e2) = do
          s1 <- toStr' e1
          s2 <- toStr' e2
          return $ "(" ++ s1 ++ " " ++ s2 ++ ")"
        toStr' (Lam f) = do
          i <- get
          modify (+ 1)
          s <- toStr' (f (Lit i))
          return $ "\\x" ++ show i ++ " " ++ s

instance Show Expr where
  show e = evalState (toStr m e) m
    where m = 2 + maxLit e

-- Examples
ex2, ex3, ex4 :: Expr

ex2 = Lam(\a -> Lam(\b -> App a (App b (Lit 3))))
ex3 = Lam(\a -> Lam(\b -> Lam(\c -> App a (App b c))))
ex4 = Lam(\a -> Lam(\b -> Lam(\c -> Lam(\d -> App (App a b) (App c d)))))

check :: Expr -> IO ()
check e = putStrLn(show e ++ " ===> \n" ++ show (rot e) ++ "\n")

main = check ex2 >> check ex3 >> check ex4

with the following result:

\x5 \x6 (x5 (x6 3)) ===> 
\x5 \x6 (x6 (x5 3))

\x2 \x3 \x4 (x2 (x3 x4)) ===> 
\x2 \x3 \x4 (x4 (x2 x3))

\x2 \x3 \x4 \x5 ((x2 x3) (x4 x5)) ===> 
\x2 \x3 \x4 \x5 ((x5 x2) (x3 x4))

(Don't be fooled by the similar-looking variable names. This is the rotation you seek, modulo alpha-conversion.)

Answer 3

Yes, I'm posting another answer. And it still might not be exactly what you're looking for. But I think it might be of use nonetheless. It's in Haskell.

data LExpr = Lambda Char LExpr
           | Atom Char
           | App LExpr LExpr

instance Show LExpr where
    show (Atom c) = [c]
    show (App l r) = "(" ++ show l ++ " " ++ show r ++ ")"
    show (Lambda c expr) = "(λ" ++ [c] ++ ". " ++ show expr ++ ")"

So here I cooked up a basic algebraic data type for expressing lambda calculus. I added a simple, but effective, custom Show instance.

ghci> App (Lambda 'a' (Atom 'a')) (Atom 'b')
((λa. a) b)

For fun, I threw in a simple reduce method, with helper replace. Warning: not carefully thought out or tested. Do not use for industrial purposes. Cannot handle certain nasty expressions. :P

reduce (App (Lambda c target) expr) = reduce $ replace c (reduce expr) target
reduce v = v

replace c expr av@(Atom v)
    | v == c    = expr
    | otherwise = av
replace c expr ap@(App l r)
                = App (replace c expr l) (replace c expr r)
replace c expr lv@(Lambda v e)
    | v == c    = lv
    | otherwise = (Lambda v (replace c expr e))

It seems to work, though that's really just me getting sidetracked. (it in ghci refers to the last value evaluated at the prompt)

ghci> reduce it
b

So now for the fun part, rotate. So I figure I can just peel off the first layer, and if it's a Lambda, great, I'll save the identifier and keep drilling down until I hit a non-Lambda. Then I'll just put the Lambda and identifier right back in at the "last" spot. If it wasn't a Lambda in the first place, then do nothing.

rotate (Lambda c e) = drill e
    where drill (Lambda c' e') = Lambda c' (drill e') -- keep drilling
          drill e' = Lambda c e'       -- hit a non-Lambda, put c back
rotate e = e

Forgive the unimaginative variable names. Sending this through ghci shows good signs:

ghci> Lambda 'a' (Atom 'a')
(λa. a)
ghci> rotate it
(λa. a)
ghci> Lambda 'a' (Lambda 'b' (App (Atom 'a') (Atom 'b')))
(λa. (λb. (a b)))
ghci> rotate it
(λb. (λa. (a b)))
ghci> Lambda 'a' (Lambda 'b' (Lambda 'c' (App (App (Atom 'a') (Atom 'b')) (Atom 'c'))))
(λa. (λb. (λc. ((a b) c))))
ghci> rotate it
(λb. (λc. (λa. ((a b) c))))