箭头中的可观察递归（或绑定）答案

【问题标题】：Observable recursion (or binding) in Arrows箭头中的可观察递归（或绑定）
【发布时间】：2016-06-26 17:52:12
【问题描述】：

我正在尝试找到一种方法来翻译正常的递归符号，例如作为 |fib|功能如下箭头，保留尽可能多的递归符号的结构尽可能。另外我会喜欢检查箭头。为此，我创建了一个包含每个 Arrow{..} 类的构造函数：

谎言：

fib 0 = 0
fib 1 = 1
fib n = fib (n-2) + fib (n-1)

我的 R 数据类型，该数据类型的实例由映射组成到适当的构造函数：

data R x y where
  -- Category
  Id       :: R a a
  Comp     :: R b c    -> R a b          -> R a c
  -- Arrow
  Arr      :: (a -> b) -> R a b
  Split    :: R b c    -> R b' c'        -> R (b,b') (c,c')
  Cache    :: (a -> a -> Bool) -> R a a
  -- ArrowChoice
  Choice   :: R b c -> R b' c' -> R (Either b b') (Either c c')
  -- ArrowLoop
  Loop     :: R (b, d) (c, d)  -> R b c
  -- ArrowApply
  Apply    :: R (R b c, b) c

翻译|fib|上面的函数首先导致以下定义。然而，由于 proc n on，这是不允许的 |fibz| 的声明的 RHS。我知道箭头符号阻止了这一点，但根本原因是什么这个？

fib' :: (ArrowChoice r, ArrowLoop r) => r Int Int
fib' = proc x -> do
  rec fibz <- proc n -> case n of
                          0  -> returnA -< 0
                          1  -> returnA -< 1
                          n' -> do l <- fibz -< (n'-2)
                                   r <- fibz -< (n'-1)
                                   returnA -< (l+r)
  fibz -<< x

重写上面的函数以使用 let 语句编译。然而，这里出现了我的第二个问题。我希望能够检查递归发生的地方。然而，在这种情况下 |fibz|是一个无限树。我想将递归捕获到 fibz，我希望rec 能结合|loop|帮助我但也许我错了？

fib'' :: (ArrowChoice r, ArrowLoop r, ArrowApply r) => r Int Int
fib'' = proc x -> do
  let fibz = proc n -> case n of
                          0  -> returnA -< 0
                          1  -> returnA -< 1
                          n' -> do l <- fibz -< (n'-2)
                                   r <- fibz -< (n'-1)
                                   returnA -< (l+r)
  fibz -<< x

基本上，可以观察到这种递归吗？（也许即使在箭头符号的范围内）我也许可以添加另一个构造函数，如修复。也许我应该能够观察变量的绑定，以便引用它们成为可能。不过，这将超出 Arrows 的范围。

对此有什么想法吗？

更新 1： 我想出了这种形式，在箭头符号之外。这隐藏了app 内的递归，因此我最终得到了箭头的有限表示。但是，我仍然希望能够例如将app 内的fib 调用替换为fib 的优化版本。

fib :: (ArrowChoice r, ArrowLoop r, ArrowApply r) => r Int Int
fib
  = (arr
       (\ n ->
          case n of
              0 -> Left ()
              1 -> Right (Left ())
              n' -> Right (Right n'))
       >>>
       (arr (\ () -> 0) |||
          (arr (\ () -> 1) |||
             (arr (\ n' -> (n', n')) >>>
                (first ( arr (\ n' -> app (fib, n' - 2))) >>>
                   arr (\ (l, n') -> (n', l)))
                  >>>
                  (first (arr (\ n' -> app (fib, n' - 1))) >>>
                     arr (\ (r, l) -> (l + r)))))))

此代码对应于以下箭头符号：

fib :: (ArrowChoice r, ArrowLoop r, ArrowApply r) => r Int Int
fib  = proc n ->
   case n of
     0  -> returnA -< 0
     1  -> returnA -< 1
     n' -> 
           do l <- fib -<< (n'-2)
              r <- fib -<< (n'-1)
              returnA -< (l+r)

【问题讨论】：

你会如何将fib 写成R？
@SjoerdVisscher 我更新了问题以将fib 包含在R 中。（但使用类方法）
reddit 正在同时进行讨论。

标签： haskell recursion arrows

【解决方案1】：

你可以用循环的形式写fib，例如这样：

fib'' :: (ArrowChoice r, ArrowLoop r, ArrowApply r) => r Int Int
fib'' = loop $ proc (i, r) -> do
    i' <- r -<< i
    returnA -< (i', proc j -> case j of
        0 -> returnA -< 0
        1 -> returnA -< 1
        _ -> do
            a <- r -< j-2
            b <- r -< j-1
            returnA -< a + b)

但这实际上只是为一个不需要它的问题引入了一个人为循环，而且在可观察性方面也不会给你带来太多好处。你可以说存在某种循环，但我认为不可能真正确定递归发生的位置。

在具体化表示中，对其他箭头的任何调用本质上都是“内联”的，这包括对同一箭头的调用。您无法真正检测到这些呼叫站点，更不用说找出正在呼叫的箭头。箭头具体化的另一个问题是，很多关于输入如何传递的有趣信息在Arr 黑洞中丢失了。

我当然不是箭专家，我希望有人证明我错了，但我倾向于认为你想要实现的目标是不可能可靠地做到的，或者至少是非常不切实际的。我能想到的可以帮助您转发的一种资源是论文 Type-Safe Observable Sharing in Haskell 和 data-reify 包。

【讨论】：

【解决方案2】：

您可以使用 Category 完全具体化 fib，只要您可以定义函数以将代码保存到磁盘并重新加载它。虽然有点丑。

{-# LANGUAGE GADTs, RankNTypes #-}

module Main where

import Control.Category

data RRef s1 s2 = RRef Int

data R s1 s2 where
  Id :: forall s. R s s
  Compose :: forall s1 s2 s3. R s2 s3 -> R s1 s2 -> R s1 s3
  Lit :: forall s a. a -> R s (a,s)
  Dup :: forall s a. R (a,s) (a,(a,s))
  Drop :: forall s b. R (b,s) s
  Add :: forall s a. Num a => R (a,(a,s)) (a,s)
  Decrement :: forall s. R (Int,s) (Int,s)
  Deref :: forall s1 s2. RRef s1 s2 -> R s1 s2
  Rec :: forall s1 s2. (RRef s1 s2 -> R s1 s2) -> R s1 s2
  IsZero :: forall s. R (Int,s) (Bool,s)
  If :: forall s1 s2. R s1 s2 -> R s1 s2 -> R (Bool,s1) s2
  Swap :: forall s a b. R (a,(b,s)) (b,(a,s))
  Over :: forall s a b. R (a,(b,s)) (a,(b,(a,s)))
  Rot :: forall s a b c. R (a,(b,(c,s))) (b,(c,(a,s)))

instance Category R where
  id = Id
  (.) = Compose

fib :: R (Int,()) (Int,())
fib =
  Lit 0 >>>
  Lit 1 >>>
  Rot >>>
  Rot >>>
  Rec (\ref ->
    Dup >>> IsZero >>> (
      If
        (Drop >>> Swap >>> Drop)
        (Decrement >>> Rot >>> Rot >>> Over >>> Add >>> Rot >>> Rot >>> (Deref ref))
    )
  )

R 这里是一个带索引的 Monoid，结果证明它与 Category 相同。 R 的两个类型参数表示操作前后堆栈的类型签名。堆栈作为程序堆栈，就像在汇编代码中一样。堆栈类型中的元组形成了一个异构列表来键入堆栈上的每个元素。所有操作（If 除外）都采用零参数并仅操作堆栈。 If 接受两个代码块并返回不带参数且仅操作堆栈的代码。

Rec 用于递归。解释器将为递归函数找到一个唯一的名称（作为整数），然后递归函数将使用 Deref 引用该名称以连接回自身形成递归。

这可以被认为是一种像 Forth 一样的串联编程语言（作为 EDSL），除了它对堆栈上的值具有类型安全性。

【讨论】：