haskell - reglamento - ley de disciplina del ejercito y fuerza aerea mexicanos

¿Las listas son inductivas o coinductivas en Haskell?

Question

Así que últimamente he estado leyendo un poco sobre la coinducción, y ahora me pregunto: ¿son las listas de Haskell inductivas o coinductivas? También he oído que Haskell no distingue a los dos, pero si es así, ¿cómo lo hacen formalmente?

Las listas se definen de forma inductiva, data [a] = [] | a : [a] data [a] = [] | a : [a] , sin embargo, se puede usar de forma coinductiva, ones = a:ones . Podemos crear listas infinitas. Sin embargo, podemos crear listas finitas. Entonces, ¿cuáles son?

Relacionado está en Idris, donde el tipo List a es estrictamente un tipo inductivo y, por lo tanto, es solo de listas finitas. Se define similar a cómo está en Haskell. Sin embargo, Stream a es un tipo coinductor, modelando una lista infinita. Se define como (o, mejor dicho, la definición es equivalente a) la codata Stream a = a :: (Stream a) . Es imposible crear una lista infinita o un flujo finito. Sin embargo, cuando escribo la definición

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

Obtengo el comportamiento que espero de las listas de Haskell, a saber, que puedo hacer estructuras tanto finitas como infinitas.

Así que permítanme resumirlas en algunas preguntas básicas:

1. ¿Haskell no distingue entre los tipos inductivos y coinductivos? Si es así, ¿cuál es la formalización para eso? Si no, ¿cuál es [a]?

2. ¿Es HList coinductivo? Si es así, ¿cómo puede un tipo coinductivo contener valores finitos?

3. ¿Qué pasa si definimos los data HList'' a = L (List a) | R (Stream a) data HList'' a = L (List a) | R (Stream a) ? ¿Qué sería eso considerado y / o sería útil solo para HList ?

Answer 1

1. Debido a la pereza, los tipos de Haskell son tanto inductivos como coinductores, o no hay una distinción formal entre datos y códigos. Todos los tipos recursivos pueden contener un anidado infinito de constructores. En idiomas como Idris, Coq, Agda, etc., una definición como ones = 1 : ones es rechazada por el comprobador de terminación. La pereza significa que las ones se pueden evaluar en un paso a 1 : ones , mientras que las otras lenguas solo se evalúan en forma normal y ones que no tienen una forma normal.

2. "Coinductivo" no significa "necesariamente infinito", significa "definido por cómo se deconstruye", mientras que inductivo significa "definido por cómo se construye". Creo que this es una excelente explicación de la sutil diferencia. Seguramente usted estaría de acuerdo en que el tipo

   codata A : Type where MkA : A

   no puede ser infinito

3. Esto es interesante, a diferencia de HList , que nunca puede "saber" si es finito o infinito (específicamente, puede descubrir en tiempo finito si una lista es finita, pero no puede calcular que es infinito) , HList'' le ofrece una forma sencilla de decidir en tiempo constante si su lista es finita o infinita.

Answer 2

En un lenguaje total como Coq o Agda, los tipos inductivos son aquellos cuyos valores se pueden demoler en un tiempo finito. Las funciones inductivas deben terminar. Los tipos coinductivos, por otro lado, son aquellos cuyos valores se pueden construir en un tiempo finito. Las funciones coinductivas deben ser productivas.

Los sistemas que están destinados a ser útiles como asistentes de prueba (como Coq y Agda) deben ser totales, porque la no terminación hace que un sistema sea lógicamente inconsistente. Pero exigir que todas las funciones sean totales e inductivas hace imposible trabajar con estructuras infinitas, por lo que se inventó la coinducción.

Por lo tanto, el propósito de los tipos inductivos y coinductivos es rechazar programas que no terminen. Aquí hay un ejemplo en Agda de una función que se rechaza debido a la condición de productividad. (La función que pasa para filter podría rechazar todos los elementos, por lo que podría estar esperando para siempre el siguiente elemento de la secuencia resultante).

filter : {A : Set} -> (A -> Bool) -> Stream A -> Stream A
filter f xs with f (head xs)
... | true = head xs :: filter f (tail xs)
... | false = filter f (tail xs)  -- unguarded recursion

Ahora, Haskell no tiene noción de tipos inductivos o coinductores. La pregunta "¿Es este tipo inductivo o coinductor?" no es significativo ¿Cómo se escapa Haskell sin hacer la distinción? Bueno, Haskell nunca tuvo la intención de ser consistente como lógica en primer lugar. Es un lenguaje parcial, lo que significa que se le permite escribir funciones no terminantes y no productivas: no hay comprobador de terminación ni comprobador de productividad. Uno puede debatir la sabiduría de esta decisión de diseño, pero ciertamente hace redundantes la inducción y la coinducción.

En cambio, los programadores de Haskell están acostumbrados a razonar informalmente sobre la terminación / productividad de un programa. La pereza nos permite trabajar con infinitas estructuras de datos, pero no recibimos ninguna ayuda de la máquina para garantizar que nuestras funciones sean totales.

Answer 3

Para interpretar la recursión a nivel de tipo, es necesario encontrar un "punto fijo" para el functor de lista con valores de CPO

F X = (1 + A_bot * X)_bot

Si razonamos de forma inductiva, queremos que el punto fijo sea "menor". Si coinductivamente, "mayor".

Técnicamente, esto se hace trabajando en la subcategoría de incrustación-proyección de CPO_bot, tomando, por ejemplo, el valor "menor" del diagrama de incrustaciones.

0_bot |-> F 0_bot |-> F (F 0_bot) |-> ...

Generalizando el teorema del punto fijo de Kleene. Para los "más grandes" tomaríamos el límite del diagrama de las proyecciones.

0_bot <-| F 0_bot <-| F (F 0_bot) <-| ...

Sin embargo, resulta que lo "menos" es isomorfo a lo "más grande", para cualquier F Este es el teorema de "bilimit" (véase, por ejemplo, el documento de encuesta de "Teoría del dominio" de Abramsky).

Tal vez sorprendentemente, resulta que el sabor inductivo o coinductor proviene de los levantamientos aplicados por F lugar de los puntos fijos más pequeños. Por ejemplo, si x es el producto aplastado y # es la suma aplastada,

F X = 1_bot # (A_bot x X)

tendría como bilimit el conjunto de listas finitas (hasta iso).

[Espero haber acertado con las maniobras; estas son difíciles ;-)]