9

我正在尝试找到一种方法来翻译正常的递归符号，例如 |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| 上面的函数首先导致以下定义。然而，由于 |fibz| 的声明的 RHS 上的 proc n，这是不允许的。我知道箭头符号的语法阻止了这一点，但其根本原因是什么？

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，因此我最终得到了箭头的有限表示。但是，我仍然希望能够例如将对fibinside的调用替换app为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)
4

2 回答 2

3

您可以用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黑洞中丢失了。

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

于 2012-10-12T05:10:24.623 回答
0

您可以使用 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），除了它对堆栈上的值具有类型安全性。

于 2016-06-26T09:41:22.387 回答