Observable recursion (or binding) in Arrows

Question

I am trying to find a way to translate normal recursive notation such as the |fib| function below to an arrow, retaining as much of the structure of the recursive notation as possible. In addition I would like to inspect the arrow. For this I created a datatype containing a constructor for each Arrow{..} class:

Fib:

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

My R datatype, the instances for this datatype consist of the mapping to the appropriate constructor:

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

Translating the |fib| function from above first resulted in the following definition. It is not allowed however due to the proc n on the RHS of the declaration for |fibz|. I know that the grammar of the Arrow Notation prevents this, but what is the underlying reason for this?

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

Rewriting the function above to use a let statement compiles. However, here my second problem arises. I want to be able to inspect the recursion where it happens. However, in this case |fibz| is an infinite tree. I would like to capture the recursion into fibz, I hoped the rec would help me with that in combination with |loop| but maybe I am wrong?

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

Basically, is it possible to observe this kind of recursion? (Perhaps even within the boundaries of Arrow Notation) I could perhaps add another constructor like fix. Maybe I should be able to observe the binding of variables so that referring to them becomes possible. This would fall outside the scope of Arrows though.

Any thoughts on this?

Update 1: I come up with this form, outside of arrow notation. This hides the recursion inside the app and therefore I end up with a finite representation of the Arrow. However, I still want to be able to e.g. replace the call to fib inside app to a an optimised version of 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)))))))                                 

This code corresponds with the following in arrow notation:

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)

Answer 1

You can write fib in terms of loop for example like this:

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)

But this is really just introducing an artificial loop to a problem that doesn't need it, and it doesn't really buy you much in terms of observability either. You can tell that some kind of loop exists, but I think it's impossible to really pinpoint the where the recursion takes place.

In the reified representation any calls to other arrows will essentially be "inlined" and this includes calls to the same arrow. You can't really detect these call sites to begin with, not to mention finding out which arrow is being called. Another problem with arrow reification is that a lot of the interesting information about how inputs are passed around is lost inside the Arr blackhole.

I'm certainly no expert on arrows and I hope someone proves me wrong, but I'm inclined to think that what you are trying to achieve is impossible to do reliably or at least highly impractical. One resource that I can think of that might help you forward is the paper Type-Safe Observable Sharing in Haskell and the data-reify package.