ejemplos - ejercicios recursivos en haskell

¿Cuál es el tipo de catamorfismo(pliegue) para los tipos recursivos no regulares?

Question

Muchos catamorfismos parecen ser bastante simples, en su mayoría reemplazando cada constructor de datos con una función personalizada, por ejemplo,

data Bool = False | True
foldBool :: r -- False constructor
-> r -- True constructor
-> Bool -> r
data Maybe a = Nothing | Just a
foldMaybe :: b -- Nothing constructor
-> (a -> b) -- Just constructor
-> Maybe a -> b
data List a = Empty | Cons a (List a)
foldList :: b -- Empty constructor
-> (a -> b -> b) -- Cons constructor
-> List a -> b

Sin embargo, lo que no me queda claro es qué sucede si se utiliza el mismo constructor de tipo, pero con un argumento de tipo diferente. Por ejemplo, en lugar de pasar una List a a Cons , ¿qué pasa con

data List a = Empty | Cons a (List (a,a))

O, tal vez un caso más loco:

data List a = Empty | Cons a (List (List a))
foldList :: b -- Empty constructor
-> ??? -- Cons constructor
-> List a -> b

Las dos ideas plausibles que tengo para el ??? parte son

• (a -> b -> b) , es decir, reemplazando recursivamente todas las aplicaciones del constructor de listas)
• (a -> List b -> b) , es decir, simplemente reemplazando todas las aplicaciones de List a .

¿Cuál de los dos sería correcto y por qué? ¿O sería algo completamente diferente?

Answer 1

Esta es una respuesta parcial, solamente.

El problema que plantea el OP es: ¿cómo definir fold / cata en el caso de tipos recursivos no regulares?

Ya que no confío en mí mismo para hacer esto bien, recurriré a preguntar a Coq. Empecemos por un tipo de lista recursiva simple y regular.

Inductive List (A : Type) : Type :=
| Empty: List A
| Cons : A -> List A -> List A
.

Nada especial aquí, la List A se define en términos de la List A (Recuerda esto: volveremos a hacerlo).

¿Qué pasa con la cata ? Vamos a consultar el principio de inducción.

> Check List_rect.
forall (A : Type) (P : List A -> Type),
P (Empty A) ->
(forall (a : A) (l : List A), P l -> P (Cons A a l)) ->
forall l : List A, P l

Veamos. Lo anterior explota los tipos dependientes: P depende del valor real de la lista. Simplemente simplifiquémoslo manualmente en el caso de que la P list sea ​​un tipo B constante. Obtenemos:

forall (A : Type) (B : Type),
B ->
(forall (a : A) (l : List A), B -> B) ->
forall l : List A, B

que se puede escribir de manera equivalente como

forall (A : Type) (B : Type),
B ->
(A -> List A -> B -> B) ->
List A -> B

Lo que es foldr excepto que la "lista actual" también se pasa al argumento de la función binaria, no es una diferencia importante.

Ahora, en Coq podemos definir una lista de otra manera sutilmente diferente:

Inductive List2 : Type -> Type :=
| Empty2: forall A, List2 A
| Cons2 : forall A, A -> List2 A -> List2 A
.

Se ve del mismo tipo, pero hay una profunda diferencia. Aquí no estamos definiendo el tipo List A en términos de la List A Más bien, estamos definiendo una función de tipo List2 : Type -> Type en términos de List2 . El punto principal de esto es que las referencias recursivas a List2 no tienen que aplicarse a A ; el hecho de que arriba lo hacemos es solo un incidente.

De todos modos, veamos el tipo para el principio de inducción:

> Check List2_rect.
forall P : forall T : Type, List2 T -> Type,
(forall A : Type, P A (Empty2 A)) ->
(forall (A : Type) (a : A) (l : List2 A), P A l -> P A (Cons2 A a l)) ->
forall (T : Type) (l : List2 T), P T l

List2 T argumento List2 T de P como lo hicimos antes, básicamente asumiendo que P es constante en él.

forall P : forall T : Type, Type,
(forall A : Type, P A ) ->
(forall (A : Type) (a : A) (l : List2 A), P A -> P A) ->
forall (T : Type) (l : List2 T), P T

Equitativamente reescrito

forall P : (Type -> Type),
(forall A : Type, P A) ->
(forall (A : Type), A -> List2 A -> P A -> P A) ->
forall (T : Type), List2 T -> P T

Lo que corresponde aproximadamente, en notación Haskell.

(forall a, p a) -> -- Empty
(forall a, a -> List2 a -> p a -> p a) -> -- Cons
List2 t -> p t

No es tan malo: el caso base ahora tiene que ser una función polimórfica, como lo es Empty en Haskell. Tiene algun sentido De manera similar, el caso inductivo debe ser una función polimórfica, tanto como lo es Cons . Hay una lista List2 a argumento, pero podemos ignorarlo, si queremos.

Ahora, lo anterior sigue siendo un tipo de pliegue / cata en un tipo regular . ¿Qué pasa con los no regulares? yo estudiaré

data List a = Empty | Cons a (List (a,a))

que en Coq se convierte en:

Inductive List3 : Type -> Type :=
| Empty3: forall A, List3 A
| Cons3 : forall A, A -> List3 (A * A) -> List3 A
.

con principio de inducción:

> Check List3_rect.
forall P : forall T : Type, List3 T -> Type,
(forall A : Type, P A (Empty3 A)) ->
(forall (A : Type) (a : A) (l : List3 (A * A)), P (A * A) l -> P A (Cons3 A a l)) ->
forall (T : Type) (l : List3 T), P T l

Eliminando la parte "dependiente":

forall P : (Type -> Type),
(forall A : Type, P A) ->
(forall (A : Type), A -> List3 (A * A) -> P (A * A) -> P A ) ->
forall (T : Type), List3 T -> P T

En notación Haskell:

 (forall a. p a) -> -- empty
(forall a, a -> List3 (a, a) -> p (a, a) -> p a ) -> -- cons
List3 t -> p t

Aparte del List3 (a, a) adicional List3 (a, a) , este es un tipo de pliegue.

Por último, ¿qué pasa con el tipo OP?

data List a = Empty | Cons a (List (List a))

Por desgracia, Coq no acepta el tipo

Inductive List4 : Type -> Type :=
| Empty4: forall A, List4 A
| Cons4 : forall A, A -> List4 (List4 A) -> List4 A
.

ya que la ocurrencia interna de List4 no está en una posición estrictamente positiva. Probablemente, este es un indicio de que debo dejar de ser perezoso y usar Coq para hacer el trabajo y comenzar a pensar en las F-álgebras involucradas por mi cuenta ... ;-)