Haskell: Común Corecursive Falacias

Question

Así que estaba pensando en un algoritmo de distancia gráfico de esta noche, y se le ocurrió esta mientras conducía en el coche:

module GraphDistance where 
import Data.Map 

distance :: (Ord a) => a -> Map a [a] -> Map a Int 
distance a m = m' 
    where m' = mapWithKey d m 
     d a' as = if a == a' then 0 else 1 + minimum (Prelude.map (m'!) as) 

Al principio, yo era bastante orgulloso de mí mismo, ya que parecía tan elegante. Pero luego me di cuenta de que no funcionaría: la corecursion podría quedarse atascada en en un bucle.

tuve que codificarlo hasta convencerme:

ghci> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])] 
fromList [(0,1),(1,0),(2,^CInterrupted. 

Pero ahora creo que he más o menos pensado bien.

¿Hay una lista de errores comunes y anti patrones cuando se trata de datos corecursive que puedo leer, para que pueda entrenar mi cerebro para pensar corecursively? La experiencia me ha capacitado bastante bien para pensar en datos no coherentes , pero me gustaría aprender de los demás errores si puedo.

Answer 1

Bueno, en realidad solo hay un error fundamental cuando se trata de datos corecursive, ¡y eso es usar descuidadamente la recursión en él!

Corecursion implica que los datos se generan incrementalmente en algún sentido. Su función de distancia gráfica es instructiva aquí, porque parece que debería funcionar, entonces piense dónde debe estar la parte incremental: El punto de partida es una distancia de 0 desde un nodo a sí mismo, de lo contrario uno mayor que la distancia mínima entre sus propios vecinos inmediatos. Por lo tanto, cabría esperar que cada valor de distancia sea incremental, lo que significa que necesitamos que sean ellos mismos convenientemente correlativos.

La recursividad en cuestión, entonces, se está produciendo debido a la combinación de (+) y minimum: la hora de encontrar el mínimo, 1 siempre habrá menos de 1 + n, sin tener que preocuparse acerca de lo que es n ... pero no hay manera para comparar Int s sin calcular todo el valor.

En resumen, el algoritmo espera poder comparar cuántas veces (1 +) se aplicó a 0 solo hasta donde sea necesario; es decir, quiere números naturales perezosos definidos usando "cero" y "sucesor".

He aquí:

data Nat = Z | S Nat 

natToInt :: Nat -> Int 
natToInt Z = 0 
natToInt (S n) = 1 + natToInt n 

instance Show Nat where show = show . natToInt 

instance Eq Nat where 
    Z == Z = True 
    (S n1) == (S n2) = n1 == n2 
    _ == _ = False 

    Z /= Z = False 
    (S n1) /= (S n2) = n1 /= n2 
    _ /= _ = True 


instance Ord Nat where 
    compare Z Z = EQ 
    compare Z (S _) = LT 
    compare (S _) Z = GT 
    compare (S n1) (S n2) = compare n1 n2 

Y luego, en GHCi:

> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])] 
fromList [(0,1),(1,0),(2,1),(3,2)] 

La prueba de que el algoritmo funciona ^[0]; su implementación fue simplemente incorrecta.

---

Ahora, como una ligera variación, vamos a aplicar el algoritmo para un gráfico diferente:

> distance 1 $ fromList [(0,[1]),(1,[0]),(2,[3]),(3,[2])] 

... ¿qué esperamos esto que ver? ¿Cuál es la distancia desde el nodo 1 para los nodos 2 o 3?

Correr en GHCi tiene la consecuencia obvia:

fromList [(0,1),(1,0),(2,^CInterrupted. 

Sin embargo, El algoritmo funciona correctamente en este gráfico. ¿Puedes ver el problema? ¿Por qué colgó en GHCi?

---

En resumen, es necesario distinguir claramente entre dos formas que no se pueden mezclar libremente:

• perezoso, posiblemente infinitos datos, generados corecursively
• datos finitos, consumido de forma recursiva

Ambas formas se pueden transformar de forma independiente de la estructura (por ejemplo, map funciona en listas finitas e infinitas). Codata se puede consumir de forma incremental, impulsado por un algoritmo corecursive; los datos se pueden generar recursivamente, limitados por un algoritmo recursivo.

Lo que no se puede do es consumir codata recursivamente (por ejemplo, doblar a la izquierda una lista infinita) o generar datos corecursively (raro en Haskell, debido a la pereza).

[0]: En realidad, fallará en algunas entradas (por ejemplo, algunos gráficos desconectados), pero eso es un problema diferente.