useful una tipos tag qué que para metadescripción importantes ejemplo cual haskell functional-programming terminology fold

haskell - una - ¿Qué constituye un pliegue para tipos distintos de la lista?



title en seo (4)

Considere una lista de enlaces únicos. Se ve algo así como

data List x = Node x (List x) | End

Es natural definir una función de plegado como

reduce :: (x -> y -> y) -> y -> List x -> y

En cierto sentido, reduce f x0 reemplaza cada Node con f y cada End con x0 . Esto es a lo que el Preludio se refiere como un doblez .

Ahora considere un simple árbol binario:

data Tree x = Leaf x | Branch (Tree x) (Tree x)

Es igualmente natural definir una función como

reduce :: (y -> y -> y) -> (x -> y) -> Tree x -> y

Tenga en cuenta que esta reducción tiene un carácter bastante diferente; mientras que el basado en listas es intrínsecamente secuencial, este nuevo basado en árboles tiene más de una sensación de dividir y vencer. Incluso podrías imaginarte arrojar algunos combinators par allí. (¿Dónde colocarías tal cosa en la versión de la lista?)

Mi pregunta: ¿esta función todavía está clasificada como un "pliegue", o es algo más? (¿Y si es así, qué es?)

Básicamente cada vez que alguien habla de plegamiento, siempre hablan de listas plegables, que es intrínsecamente secuencial. Me pregunto si "secuencial" es parte de la definición de lo que es un pliegue, o si esto es simplemente una propiedad fortuita del ejemplo de plegado más comúnmente utilizado.

Un doblez para cada ocasión

De hecho, podemos llegar a una noción genérica de plegamiento que se puede aplicar a un montón de diferentes tipos. Es decir, podemos definir sistemáticamente una función de fold para listas, árboles y más.

Esta noción genérica de fold corresponde a los catamorphisms @pelotom mencionados en su comentario.

Tipos recursivos

La idea clave es que estas funciones de fold se definen sobre tipos recursivos . En particular:

data List a = Cons a (List a) | Nil data Tree a = Branch (Tree a) (Tree a) | Leaf a

Ambos tipos son claramente recursivos: List en el caso Cons y Tree en el caso Branch .

Puntos fijos

Al igual que las funciones, podemos reescribir estos tipos utilizando puntos fijos. Recuerde la definición de fix :

fix f = f (fix f)

De hecho, podemos escribir algo muy similar para los tipos, excepto que tiene que tener un envoltorio constructor adicional:

newtype Fix f = Roll (f (Fix f))

Al igual que fix define el punto fijo de una función , esto define el punto fijo de un funtor . Podemos expresar todos nuestros tipos recursivos usando este nuevo tipo de Fix .

Esto nos permite reescribir los tipos de List siguiente manera:

data ListContainer a rest = Cons a rest | Nil type List a = Fix (ListContainer a)

Básicamente, Fix nos permite anidar ListContainer a profundidades arbitrarias. Entonces podríamos tener:

Roll Nil Roll (Cons 1 (Roll Nil)) Roll (Cons 1 (Roll (Cons 2 (Roll Nil))))

que corresponden a [] , [1] y [1,2] respectivamente.

Ver que ListContainer es un Functor es fácil:

instance Functor (ListContainer a) where fmap f (Cons a rest) = Cons a (f rest) fmap f Nil = Nil

Creo que el mapeo de ListContainer a List es bastante natural: en lugar de recurrir explícitamente, hacemos que la parte recursiva sea una variable. Luego usamos Fix para llenar esa variable según corresponda.

También podemos escribir un tipo análogo para Tree .

Puntos fijos de "desenvolver"

Entonces, ¿por qué nos preocupa? Podemos definir fold para tipos arbitrarios escritos usando Fix . En particular:

fold :: Functor f => (f a -> a) -> (Fix f -> a) fold h = h . fmap (fold h) . unRoll where unRoll (Roll a) = a

Básicamente, todo lo que hace un pliegue es desenvolver el tipo "laminado" una capa a la vez, aplicando una función al resultado cada vez. Este "desenrollamiento" nos permite definir un pliegue para cualquier tipo recursivo y generalizar el concepto de una manera clara y natural.

Para el ejemplo de la lista, funciona así:

  1. En cada paso, desenvolvemos el Roll para obtener un Cons o un Nil
  2. Recurrimos sobre el resto de la lista usando fmap .
    1. En el caso Nil , fmap (fold h) Nil = Nil , así que simplemente devolvemos Nil .
    2. En el caso Cons , el fmap simplemente continúa el doblez sobre el resto de la lista.
  3. Al final, obtenemos un montón de llamadas anidadas para fold terminando en un Nil al igual que el foldr estándar.

Comparar tipos

Ahora veamos los tipos de las funciones de doblez. Primero, foldr :

foldr :: (a -> b -> b) -> b -> [a] -> b

Ahora, fold especializado a ListContainer :

fold :: (ListContainer a b -> b) -> (Fix (ListContainer a) -> b)

Al principio, estos se ven completamente diferentes. Sin embargo, con un poco de masaje, podemos demostrar que son lo mismo. Los dos primeros argumentos para foldr son a -> b -> b y b . Tenemos una función y una constante. Podemos pensar en b como () -> b . Ahora tenemos dos funciones _ -> b donde _ es () y a -> b . Para hacer la vida más simple, vamos a curry la segunda función que nos da (a, b) -> b . Ahora podemos escribirlos como una función única usando Either :

Either (a, b) () -> b

Esto es cierto porque dado f :: a -> c y g :: b -> c , siempre podemos escribir lo siguiente:

h :: Either a b -> c h (Left a) = f a h (Right b) = g b

Entonces ahora podemos ver foldr como:

foldr :: (Either (a, b) () -> b) -> ([a] -> b)

(Siempre somos libres de agregar paréntesis alrededor -> así siempre que sean correctos).

Ahora veamos ListContainer . Este tipo tiene dos casos: Nil , que no contiene información y Cons , que tiene tanto a como a b . Dicho de otra manera, Nil es como () y Cons es como (a, b) , entonces podemos escribir:

type ListContainer a rest = Either (a, rest) ()

Claramente esto es lo mismo que lo que utilicé en foldr arriba. Entonces ahora tenemos:

foldr :: (Either (a, b) () -> b) -> ([a] -> b) fold :: (Either (a, b) () -> b) -> (List a -> b)

Entonces, de hecho, los tipos son isomorfos, ¡solo formas diferentes de escribir lo mismo! Creo que eso es genial.

(Como nota al margen, si desea saber más sobre este tipo de razonamiento con tipos, consulte El Álgebra de tipos de datos algebraicos , una buena serie de publicaciones de blog sobre esto).

De vuelta a los árboles

Entonces, hemos visto cómo podemos definir un fold genérico para los tipos escritos como puntos fijos. También hemos visto cómo esto se corresponde directamente con foldr para las listas. Ahora veamos tu segundo ejemplo, el árbol binario. Tenemos el tipo:

data Tree a = Branch a (Tree a) (Tree a) | Leaf a

podemos reescribir esto usando Fix siguiendo las reglas que hice arriba: reemplazamos la parte recursiva con una variable de tipo:

data TreeContainer a rest = Branch rest rest | Leaf a type Tree a = Fix (TreeContainer a)

Ahora tenemos un fold árbol:

fold :: (TreeContainer a b -> b) -> (Tree a -> b)

Su foldTree original se ve así:

foldTree :: (b -> b -> b) -> (a -> b) -> Tree a -> b

foldTree acepta dos funciones; combinaremos el uno con el primer currying y luego con Either :

foldTree :: (Either (b, b) a -> b) -> (Tree a -> b)

También podemos ver cómo Either (b, b) a es isomorfo a TreeContainer ab . Tree container tiene dos casos: Branch , que contiene dos b s y Leaf , que contiene uno a .

Entonces, estos tipos de pliegues son isomorfos de la misma manera que el ejemplo de la lista.

Generalizando

Hay un patrón claro emergente. Dado un tipo de datos recursivo normal, podemos crear sistemáticamente una versión no recursiva del tipo, que nos permite expresar el tipo como un punto fijo de un funtor. Esto significa que podemos crear mecánicamente las funciones de fold para todos estos tipos diferentes; de hecho, probablemente podríamos automatizar todo el proceso usando GHC Generics o algo así.

En cierto sentido, esto significa que realmente no tenemos diferentes funciones de fold para diferentes tipos. Por el contrario, tenemos una sola función de fold que es muy polimórfica.

Más

Primero entendí por completo estas ideas en una charla ofrecida por Conal Elliott. Esto entra en más detalles y también habla de unfold , que es doble para fold .

Si desea ahondar en este tipo de cosas aún más profundamente, lea el fantástico documento "Programación funcional con plátanos, lentes, sobres y alambre de púas" . Entre otras cosas, esto introduce las nociones de "catamorfismos" y "anamorphisms" que corresponden a pliegues y despliegues.

Álgebras (y Coalgebras)

Además, no puedo resistirme a agregar un complemento: P. Puedes ver algunas similitudes interesantes entre la forma en que usamos Either aquí y la forma en que lo usé cuando hablo de algebras en otra respuesta SO.

De hecho, hay una conexión profunda entre fold y álgebras; además, se unfold --el doble fold antes mencionado-- está conectado a coalgebras, que son el dual de álgebras. La idea importante es que los tipos de datos algebraicos corresponden a "álgebras iniciales" que también definen pliegues como se indica en el resto de mi respuesta.

Puedes ver esta conexión en el tipo general de fold :

fold :: Functor f => (f a -> a) -> (Fix f -> a)

El fa -> a término parece muy familiar! Recuerde que un f-álgebra se definió como algo así como:

class Functor f => Algebra f a where op :: f a -> a

Entonces podemos pensar en fold como simplemente:

fold :: Algebra f a => Fix f -> a

Básicamente, fold solo nos permite "resumir" las estructuras definidas usando el álgebra.

Tikhon tiene problemas técnicos. Creo que trataré de simplificar lo que dijo.

El término "plegado" se ha convertido, por desgracia, ambiguo a lo largo de los años en una de dos cosas:

  1. Reducir una colección secuencialmente en algún orden. En Haskell, esto es lo que significa "doblar" en la clase Foldable , que trae larsmans.
  2. La noción que solicitó: "destrucción" (opuesto a la construcción ), "observación" o "eliminación" de un tipo de datos algebraicos de acuerdo con su estructura. También se llama catamorfismo .

Es posible definir ambas nociones genéricamente de forma que una función parametrizada sea capaz de hacerlo para una variedad de tipos. Tikhon muestra cómo hacerlo en el segundo caso.

Pero la mayoría de las veces todo el camino con Fix y las álgebras es excesivo. Hagamos una forma más simple de escribir el doblez para cualquier tipo de datos algebraicos. Utilizaremos Maybe , pairs, lists y trees como nuestros ejemplos:

data Maybe a = Nothing | Just a data Pair a b = Pair a b data List a = Nil | Cons a (List a) data Tree x = Leaf x | Branch (Tree x) (Tree x) data BTree a = Empty | Node a (BTree a) (BTree a)

Tenga en cuenta que Pair no es recursivo; el procedimiento que voy a mostrar no supone que el tipo "plegado" sea recursivo. La gente no suele llamar a este caso un "doblez", pero en realidad es el caso no recursivo del mismo concepto.

Primer paso: el doblez para un tipo dado consumirá el tipo plegado y producirá algún tipo de parámetro como resultado. Me gusta llamar a este último r (por "resultado"). Asi que:

foldMaybe :: ... -> Maybe a -> r foldPair :: ... -> Pair a b -> r foldList :: ... -> List a -> r foldTree :: ... -> Tree a -> r foldBTree :: ... -> BTree a -> r

Segundo paso: además del último argumento (el de la estructura), el doblez toma tantos argumentos como el tipo tiene constructores. Pair tiene un constructor y nuestros otros ejemplos tienen dos, entonces:

foldMaybe :: nothing -> just -> Maybe a -> r foldPair :: pair -> Pair a b -> r foldList :: nil -> cons -> List a -> r foldTree :: leaf -> branch -> Tree a -> r foldBTree :: empty -> node -> BTree a -> r

Tercer paso: cada uno de estos argumentos tiene la misma ariadidad que el constructor al que corresponde. Consideremos los constructores como funciones y escriba sus tipos (asegurándose de que las variables de tipo coincidan con las de las firmas que estamos escribiendo):

Nothing :: Maybe a Just :: a -> Maybe a Pair :: a -> b -> Pair a b Nil :: List a Cons :: a -> List a -> List a Leaf :: a -> Tree a Branch :: Tree a -> Tree a -> Tree a Empty :: BTree a Node :: a -> BTree a -> BTree a -> BTree a

Paso 4: en la firma de cada constructor, reemplazaremos todas las apariciones del tipo de datos que construye con nuestra variable de tipo r (que estamos usando en nuestras firmas de plegado):

nothing := r just := a -> r pair := a -> b -> r nil := r cons := a -> r -> r leaf := a -> r branch := r -> r -> r empty := r node := a -> r -> r -> r

Como puede ver, he "asignado" las firmas resultantes a mis variables de tipo ficticio del segundo paso. Ahora, paso 5: rellene los anteriores con las firmas de doblez del bosquejo anterior:

foldMaybe :: r -> (a -> r) -> Maybe a -> r foldPair :: (a -> b -> r) -> Pair a b -> r foldList :: r -> (a -> r -> r) -> List a -> r foldTree :: (a -> r) -> (r -> r -> r) -> Tree a -> r foldBTree :: r -> (a -> r -> r -> r) -> BTree a -> r

Ahora, estas son firmas para los pliegues de esos tipos. Tienen un orden divertido de argumentos, porque lo hice mecánicamente leyendo las declaraciones de data y los tipos de constructores, pero por alguna razón en la programación funcional es convencional poner primero los casos base en data definiciones de data pero los manejadores de casos recursivos primero en las definiciones de fold . ¡No hay problema! Vamos a reorganizarlos para hacerlos más convencionales:

foldMaybe :: (a -> r) -> r -> Maybe a -> r foldPair :: (a -> b -> r) -> Pair a b -> r foldList :: (a -> r -> r) -> r -> List a -> r foldTree :: (r -> r -> r) -> (a -> r) -> Tree a -> r foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r

Las definiciones también se pueden completar de forma mecánica. Vamos a elegir foldBTree e implementarlo paso a paso. El doblez para un tipo dado es la única función del tipo que descubrimos que cumple esta condición: doblar con los constructores del tipo es una función de identidad sobre ese tipo (obtienes el mismo resultado que el valor con el que comenzaste).

Empezaremos así:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r foldBTree = ???

Sabemos que se necesitan tres argumentos, por lo que podemos agregar variables para reflejarlos. Usaré nombres descriptivos largos:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r foldBTree branch empty tree = ???

Al BTree la declaración de data , sabemos que BTree tiene dos posibles constructores. Podemos dividir la definición en un caso para cada uno y completar las variables para sus elementos:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r foldBTree branch empty Empty = ??? foldBTree branch empty (Branch a l r) = ??? -- Let''s use comments to keep track of the types: -- a :: a -- l, r :: BTree a

Ahora, a falta de algo como undefined , la única forma de completar la primera ecuación es con el empty :

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r foldBTree branch empty Empty = empty foldBTree branch empty (Branch a l r) = ??? -- a :: a -- l, r :: BTree a

¿Cómo completamos la segunda ecuación? De nuevo, sin undefined , tenemos esto:

branch :: a -> r -> r -> r a :: a l, r :: BTree a

Si tuviéramos subfold :: BTree a -> r , podríamos hacer branch a (subfold l) (subfold r) :: r . Pero, por supuesto, podemos escribir ''subfold'' fácilmente:

foldBTree :: (a -> r -> r -> r) -> r -> BTree a -> r foldBTree branch empty Empty = empty foldBTree branch empty (Branch a l r) = branch a (subfold l) (subfold r) where subfold = foldBTree branch empty

Este es el doblez para BTree , porque foldBTree Branch Empty anyTree == anyTree . Tenga en cuenta que foldBTree no es la única función de este tipo; también hay esto:

mangleBTree :: (a -> r -> r -> r) -> r -> BTree a -> r mangleBTree branch empty Empty = empty mangleBTree branch empty (Branch a l r) = branch a (submangle r) (submangle l) where submangle = mangleBTree branch empty

Pero en general, mangleBTree no tiene la propiedad requerida; por ejemplo, si tenemos foo = Branch 1 (Branch 2 Empty Empty) Empty , se deduce que mangleBTree Branch Empty foo /= foo . Entonces mangleBTree , aunque tiene el tipo correcto, no es el doblez.

Ahora, tomemos un paso atrás de los detalles, y nos concentremos en ese último punto con el ejemplo de mangleTree . Un pliegue (en el sentido estructural, n. ° 2 en la parte superior de mi respuesta) es nada más y nada más que la función más simple y no trivial para un tipo algebraico tal que, cuando cede en los constructores del tipo como argumentos, se convierte en la función de identidad para ese tipo. (Por no trivial quiero decir que cosas como foo fz xs = xs no están permitidas).

Esto es muy significativo. Dos formas en las que me gusta pensar son las siguientes:

  1. El doblez para un tipo dado puede "ver" toda la información contenida por cualquier valor de ese tipo. (Es por eso que es capaz de "reconstruir" perfectamente cualquier valor de ese tipo desde cero utilizando los constructores del tipo).
  2. El doblez es la función más general de "consumidor" para ese tipo. Cualquier función que consuma un valor del tipo en cuestión se puede escribir de modo que las únicas operaciones que utiliza de ese tipo sean el doblez y los constructores. (Aunque las versiones solo plegables de algunas funciones son difíciles de escribir y funcionan mal, intente escribir tail :: [a] -> [a] con foldr , (:) y [] como un ejercicio doloroso).

Y el segundo punto va más allá, ya que ni siquiera necesita los constructores. Puede implementar cualquier tipo algebraico sin usar declaraciones de data o constructores, usando nada más que pliegues:

{-# LANGUAGE RankNTypes #-} -- | A Church-encoded list is a function that takes the two ''foldr'' arguments -- and produces a result from them. newtype ChurchList a = ChurchList { runList :: forall r. (a -> r -> r) -- ^ first arg of ''foldr'' -> r -- ^ second arg of ''foldr'' -> r -- ^ ''foldr'' result } -- | Convenience function: make a ChurchList out of a regular list toChurchList :: [a] -> ChurchList a toChurchList xs = ChurchList (/kons knil -> foldr kons knil xs) -- | ''toChurchList'' isn''t actually needed, however, we can make do without ''[]'' -- completely. cons :: a -> ChurchList a -> ChurchList a cons x xs = ChurchList (/f z -> f x (runlist xs f z)) nil :: ChurchList a nil = ChurchList (/f z -> z) foldr'' :: (a -> r -> r) -> r -> ChurchList a -> r foldr'' f z xs = runList xs f z head :: ChurchList a -> Maybe a head = foldr'' ((Just .) . const) Nothing append :: ChurchList a -> ChurchList a -> ChurchList a append xs ys = foldr'' cons ys xs -- | Convert a ''ChurchList'' to a regular list. fromChurchList :: ChurchList a -> [a] fromChurchList xs = runList xs (:) []

Como ejercicio, puede intentar escribir otros tipos de esta manera (que usa la extensión RankNTypes como primer ). Esta técnica se llama codificación Church , y a veces es útil en la programación real; por ejemplo, GHC usa algo llamado fusión foldr / build para optimizar el código de la lista para eliminar listas intermedias; vea esta página Haskell Wiki , y tenga en cuenta el tipo de build :

build :: (forall b. (a -> b -> b) -> b -> b) -> [a] build g = g (:) []

Excepto por el newtype , este es el mismo que mi fromChurchList arriba. Básicamente, una de las reglas que GHC usa para optimizar el código de procesamiento de listas es esta:

-- Don''t materialize the list if all we''re going to do with it is -- fold it right away: foldr kons knil (fromChurchList xs) ==> runChurchList xs kons knil

Al implementar las funciones básicas de la lista para usar internamente las codificaciones de la Iglesia, al enunciar sus definiciones agresivamente y al aplicar esta regla al código en línea, los usos anidados de funciones como el map se pueden fusionar en un ciclo cerrado.

Un doblez reemplaza a cada constructor con una función.

Por ejemplo, foldr cons nil reemplaza cada (:) con cons y [] con nil :

foldr cons nil ((:) 1 ((:) 2 [])) = cons 1 (cons 2 nil)

Para un árbol, la foldTree branch leaf reemplaza cada Branch con branch y cada Leaf con leaf :

foldTree branch leaf (Branch (Branch (Leaf 1) (leaf 2)) (Leaf 3)) = branch (branch (leaf 1) (leaf 2)) (leaf 2)

Esta es la razón por la que cada doblez acepta argumentos que tienen exactamente el mismo tipo que los constructores:

foldr :: (a -> list -> list) -> list -> [a] -> list foldTree :: (tree -> tree -> tree) -> (a -> tree) -> Tree a -> tree