旋轉的第一個參數的功能，成爲第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

OK，感謝大家誰提供了一個答案。這是我最終與之合作的解決方案。趁着這樣的事實，我知道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，因爲在演算，術語的元數可以依賴於它的參數。即沒有確定的「最後」論點。相應地更改了問題。

Answer 2

你能用普通的方式寫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)，這需要一個函數和一個列表，並且應用列表作爲參數的元素到功能。我想在這種情況下，只要取消旋轉列表並將其發送出去並不困難。我再次按照專家的意見進行更深入的回答。

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

它似乎工作，雖然這真的只是我越來越側面。 （it在ghci中是指在提示符評估的最後一個值）

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

這可能不違反人道主義組織的「合法性」，在這個意義上，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)) 

（不要用外觀相似的變量名被愚弄這是你所尋求的旋轉，模字母轉換。）

Answer 5

我想認爲你可以使用在這篇論文中描述的技術An n-ary zipWith in Haskell。

Answer 6

訣竅是標記所涉及函數的「最終」值，因爲對於正常的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 7

一種方式與模板哈斯克爾這樣做會是這樣：

有了這兩個功能：

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做這個，我對它很陌生。