将函数的第一个参数旋转为第 n 个

Question

给定一个至少有 n 参数的函数，我想旋转第一个参数，使其成为 nth 参数。例如（在无类型 lambda 演算中）：

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

等等。

你能用通用的方式写r吗？如果你知道n >= 2怎么办？

这是 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

例如，旋转应采用Lam(a => Lam(b => Lam(c => Ap(Ap(a, b), c)))) 并返回Lam(b => Lam(c => Lam(a => Ap(Ap(a, b), c))))。

Answer 1

诀窍是标记所涉及函数的“最终”值，因为对于普通的 haskell，a -> b 和 a -> (b->c) 都只是单个变量的函数。 但是，如果我们这样做，我们就可以这样做。

{-# 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

然后，看看它的实际效果：

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

如果不违反 HOAS 的“合法性”，这可能是不可能的，因为E => E 不仅必须用于对象语言中的绑定，还必须用于元语言中的计算。也就是说，这是 Haskell 中的一个解决方案。它滥用Literal 节点来放入唯一ID 以供以后替换。享受吧！

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

结果如下：

\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))

（不要被看起来相似的变量名称所迷惑。这是您寻求的旋转，模 alpha 转换。）

Answer 3

是的，我正在发布另一个答案。而且它可能仍然不是您想要的。但我认为它可能仍然有用。它在 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 ++ ")"

所以我在这里制作了一个基本的代数数据类型来表达 lambda 演算。我添加了一个简单但有效的自定义 Show 实例。

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

为了好玩，我引入了一个简单的reduce 方法，带有助手replace。警告：未经仔细考虑或测试。请勿用于工业用途。无法处理某些讨厌的表达。 :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))

这似乎奏效了，虽然这真的只是让我走神了。 （ghci 中的it 指的是在提示符处评估的最后一个值）

ghci> reduce it
b

现在是有趣的部分，rotate。所以我想我可以剥掉第一层，如果是 Lambda，那太好了，我会保存标识符并继续向下钻取，直到遇到非 Lambda。然后我将把 Lambda 和标识符放回“最后”位置。如果它一开始就不是 Lambda，那就什么都不做。

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

请原谅没有想象力的变量名称。通过 ghci 发送它显示出良好的迹象：

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

Answer 4

使用模板 haskell 的一种方法是这样的：

有这两个功能：

import Language.Haskell.TH

rotateFunc   :: Int -> Exp
rotateFunc n = LamE (map VarP vars) $ foldl1 AppE $ map VarE $ (f:vs) ++ [v]
    where vars@(f:v:vs) = map (\i -> mkName $ "x" ++ (show i)) [1..n]

getNumOfParams :: Info -> Int
getNumOfParams (VarI _ (ForallT xs _ _) _ _) = length xs + 1

然后对于具有可变数量参数的函数myF，您可以这样旋转它们：

$(return $ rotateFunc $ read $(stringE . show =<< (reify 'myF >>= return . getNumOfParams))) myF

使用 TH 肯定有更简洁的方法，我对它很陌生。

Answer 5

好的，感谢所有提供答案的人。这是我最终采用的解决方案。趁着我知道n：

rot :: Int -> [Expr] -> Expr
rot 0 xs = Lam $ \x -> foldl App x (reverse xs)
rot n xs = Lam $ \x -> rot (n - 1) (x : xs)

rot1 n = rot n []

我认为不提供n 就无法解决这个问题，因为在 lambda 演算中，一个术语的数量可能取决于它的参数。 IE。没有明确的“最后”论点。相应地改变了问题。

Answer 6

我认为您可以为此使用论文An n-ary zipWith in Haskell 中描述的技术。

Answer 7

你能用通用的方式写r吗？ 如果你知道n怎么办？

Haskell

不是普通的Haskell。您必须使用一些其他人（比我聪明得多）可能会发布的深层模板魔法。

在普通的 Haskell 中，让我们尝试编写一个类。

class Rotatable a where
    rotate :: a -> ???

到底什么是旋转类型？如果你不能编写它的类型签名，那么你可能需要模板来在你正在寻找的通用级别上进行编程（无论如何，在 Haskell 中）。

不过，将这个想法转化为 Haskell 函数很容易。

r1 f = \a -> f a
r2 f = \b -> \a -> f a b
r3 f = \b -> \c -> \a -> f a b c

等等

---

Lisp

一些 Lispy 语言有apply function (linked: r5rs)，它接受一个函数和一个列表，并将列表的元素作为参数应用到函数中。我想在这种情况下，只需取消轮换列表并将其发送出去就不会那么难了。我再次向大师寻求更深入的答案。