haskell - ¿Cómo funciona esta definición de ArrowLoop.loop?

arrows

Question

La instancia de la función para ArrowLoop contiene

loop :: ((b,d) -> (c,d)) -> (b -> c)
loop f b = let (c,d) = f (b,d) in c

Primero tengo un problema con la firma: ¿Cómo podemos obtener b -> c de (b,d) -> (c,d) ? Quiero decir, la c en la tupla resultante puede depender de ambos elementos de la entrada, ¿cómo es posible "cortar" la influencia de d ?

En segundo lugar no entiendo cómo funciona el let aquí. ¿No contiene (c,d) = f (b,d) una definición cíclica para d ? ¿De dónde viene d ? Para ser honesto, me sorprende que esta sintaxis sea válida, ya que parece que redefiniríamos d .

Quiero decir, en matemáticas esto tendría sentido, por ejemplo, f podría ser una función compleja, pero solo proporcionaría la parte b real, y tendría que elegir la parte d imaginaria de manera que no cambie cuando evalúa f (b, d), lo que lo convertiría en algún tipo de punto fijo. Pero si esta analogía se mantiene, la expresión let debe "buscar" de alguna manera ese punto fijo para d (y podría haber más de uno). Lo que me parece mágico. ¿O me parece demasiado complicado?

Answer 1

"Buscar el punto fijo" es exactamente lo que hace esto. Esta es la pereza de Haskell en acción. Ver más en Wikipedia .

Answer 2

Esto funciona de la misma manera que la definición estándar de fix funciona:

fix f = let x = f x in x

es decir, está encontrando un punto fijo exactamente de la misma manera que lo hace la fix : recursivamente.

Por ejemplo, como ejemplo trivial, considere loop (/((),xs) -> (xs, 1:xs)) () . Esto es como fix (/xs -> 1:xs) ; ignoramos nuestra entrada, y usamos la salida d (aquí xs ) como nuestra salida principal. El elemento adicional en la tupla que tiene el loop es solo para contener el parámetro de entrada y el valor de salida, ya que las flechas no pueden hacer curry. Considere cómo definiría una función factorial con fix : terminaría usando el curry, pero al usar las flechas, usaría el parámetro extra y la salida que el loop le da.

Básicamente, el loop ata un nudo, lo que permite que una flecha acceda a una salida auxiliar de sí mismo, al igual que el fix un nudo, y le da a una función acceso a su propia salida como entrada.