Ricorsione (o associazione) osservabile in Frecce

Question

Sto cercando di trovare un modo per tradurre la notazione ricorsiva normale come come | fib | funzione sotto a una freccia, conservando la maggior parte della struttura della notazione ricorsiva possibile. Inoltre vorrei come ispezionare la freccia. Per questo ho creato un tipo di dati che contiene un costruttore per ogni freccia {..} classe:

Fib:

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

mio R tipo di dati, le istanze di questo tipo di dati consistono nella mappatura al costruttore appropriato :

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 

Traducendo l'| fib | la funzione dall'alto ha avuto come risultato la seguente definizione . Non è tuttavia consentito a causa del proc n on RHS della dichiarazione per | fibz |. So che la grammatica della notazione delle frecce impedisce questo, ma qual è il motivo sottostante per questo ?

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 

Riscrivere la funzione di cui sopra per utilizzare una dichiarazione di let compila. Tuttavia, qui sorge il mio secondo problema. Voglio essere in grado di ispezionare la ricorsione dove accade. Tuttavia, in questo caso | fibz | è un albero infinito . Vorrei catturare la ricorsione in fibz, I speravo che il rec mi aiutasse con quello in combinazione con | loop | ma forse mi sbaglio?

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 

Fondamentalmente, è possibile osservare questo tipo di ricorsione? (Forse anche entro i confini di Notazione Arrow) Potrei forse aggiungere un altro costruttore come fix. Forse dovrei essere in grado di osservare il legame delle variabili in modo che il riferimento a loro sia possibile. Tuttavia, ciò non rientrerebbe nello scopo di Arrows.

Qualche idea su questo?

Aggiornamento 1: Mi viene in mente questo modulo, al di fuori della notazione a freccia. Ciò nasconde la ricorsione all'interno dello app e quindi finisco con una rappresentazione finita della freccia. Tuttavia, voglio ancora essere in grado di, ad es. sostituire la chiamata a fib all'interno di app in una versione ottimizzata di 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)))))))         

Questo codice corrisponde con quanto segue in freccia notazione:

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

È possibile scrivere fib in termini di ciclo per esempio come questo:

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) 

Ma questo è davvero solo l'introduzione un loop artificiale per un problema che non ne ha bisogno, e in realtà non ti compra molto in termini di osservabilità. Puoi dire che esiste un qualche tipo di loop, ma penso che sia impossibile individuare realmente dove si svolge la ricorsione.

Nella rappresentazione reificata tutte le chiamate ad altre frecce saranno essenzialmente "in linea" e ciò include le chiamate alla stessa freccia. In realtà non è possibile rilevare questi siti di chiamata per cominciare, per non parlare di scoprire quale freccia viene chiamata. Un altro problema con la reificazione delle frecce è che molte informazioni interessanti su come vengono passati gli input vengono perse all'interno del buco nero Arr.

Non sono certo un esperto di frecce e spero che qualcuno mi provi male, ma sono incline a pensare che ciò che stai cercando di ottenere sia impossibile da fare in modo affidabile o almeno altamente poco pratico. Una risorsa che posso pensare che potrebbe aiutarti ad avanzare è il documento Type-Safe Observable Sharing in Haskell e il pacchetto data-reify.

Answer 2

È possibile reificare completamente fib con una categoria, nella misura in cui è possibile definire le funzioni per salvare il codice su disco e caricarlo di nuovo. È un po 'brutto però.

{-# 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 ecco un Monoide indicizzato, che risulta essere la stessa cosa come Category. I due parametri di tipo su R rappresentano la firma del tipo dello stack prima e dopo un'operazione. Uno stack come stack di programmi, come nel codice assembly. Le tuple nei tipi di stack formano un elenco eterogeneo per digitare ciascuno degli elementi nello stack. Tutte le operazioni (tranne If) prendono zero parametri e semplicemente manipolano la pila. L'If prende due blocchi di codice e restituisce il codice che non richiede parametri e manipola semplicemente lo stack.

Rec viene utilizzato per la ricorsione. Un interprete potrebbe individuare un nome univoco (come numero intero) per la funzione ricorsiva, quindi la funzione ricorsiva farebbe riferimento a quel nome con Deref per ricollegarsi a se stesso formando una ricorsione.

Questo tipo di cosa può essere pensato come un linguaggio di programmazione concatenativo (come una EDSL) come Forth, eccetto che ha la sicurezza del tipo per i valori sullo stack.