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.

Answer 2

You can fully reify fib with a Category, to the extent that you can define functions to save your code to disk and load it back. It is a tiny bit ugly though.

{-# 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 here is an indexed Monoid, which turns out to be the same thing as a Category. The two type parameters to R represent the type signature of the stack before and after an operation. A stack as a program stack, like in assembly code. The tuples in the stack types form up a heterogeneous list to type each of the elements on the stack. All operations (except If) take zero parameters and just manipulate the stack. The If takes two blocks of code and returns code that takes no parameters and just manipulates the stack.

Rec is used for recursion. An interpreter would locate a unique name (as an integer) for the recursive function, then the recursive function would refer to that name with Deref to wire back to itself forming a recursion.

This can sort of thing could be thought of as a concatenative programing language (as a EDSL) like Forth, except it has type-safety for the values on the stack.