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

Question

给定一个至少具有 n 个参数的函数，我想旋转第一个参数，使其成为第 n 个参数。例如（在无类型 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

是的，我正在发布另一个答案。而且它可能仍然不完全是您正在寻找的东西。但我认为它仍然可能有用。这是在哈斯克尔。

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

现在轮到有趣的部分了，旋转。所以我想我可以剥离第一层，如果它是 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 演算中，项的元数可以取决于它的争论。即没有明确的“最后”论点。相应地改变了问题。

Answer 6

我认为您可以使用论文 Haskell 中的 n 元 zipWith 用于此目的。

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

Lispy 语言具有 apply 函数（链接：r5rs），它接受一个函数和一个列表，并将列表的元素作为参数应用于函数。我想在这种情况下，取消列表的旋转并继续发送它并不那么困难。我再次向专家们寻求更深入的答案。