箭头中可观察到的递归(或绑定)



我正试图找到一种方法来翻译正常的递归表示法,例如作为箭头下面的|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。我知道箭头符号防止了这种情况,但其根本原因是什么这

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,例如:

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和数据实体化包。

您可以用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引用该名称,以连接回自身,从而形成递归。

这可以被认为是一种级联编程语言(作为EDSL),就像Forth一样,只是它对堆栈上的值具有类型安全性。

最新更新