¿Qué punto de fijación es el tipo de lista Haskell?

Respuestas:

4

Lo correcto es configurar

data ListF a x = Nil | Cons a x

Ahora puedes escribir

newtype Mu f= Mu (forall a.(f a->a)->a)
data Nu f   = forall a. Nu a (a->f a)

En Haskell podemos observar eso Mu ListFy Nu ListFcoincidir. Entonces, puede ser cualquiera (!). (una fuente sobre este reclamo: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf )

Además, podemos probar cosas por inducción en todas las listas y obtener pruebas que funcionen siempre y cuando nos limitemos a preocuparnos por las finitas, como se describe aquí: http://www.cs.ox.ac.uk/jeremy.gibbons/ Publicaciones / fast + loose.pdf

Otras dos referencias sobre esto son:

sclv
fuente
Creo que te falta una x en esa declaración de tipo de datos ...
miniBill
2
Hay una razón por la que Jeremy llamó a ese periódico "rápido y suelto". Esta respuesta es exactamente el tipo de negación de la que estoy hablando. Es el mejor punto fijo, el final de la historia. El primer artículo vinculado de Jeremy es sobre eso, por ejemplo.
Andrej Bauer el
10

Es el punto fijo más grande, o el coalgebra final, dependiendo de cómo configure las cosas. En Haskell es imposible definir el tipo de datos de las listas finitas porque Haskell no tiene tipos inductivos, solo los coinductores. Muchas personas niegan este problema en particular.

Andrej Bauer
fuente
¿Muchas personas están en negación?
miniBill
2
Claro, me encuentro con personas que intentan probar cosas por inducción en listas, árboles, etc. en Haskell. Fingen que todos estos tipos de datos son inductivos.
Andrej Bauer
¿Y no puedes probar las cosas por inducción en las listas?
miniBill
2
No puede probar propiedades del tipo [a]en Haskell por inducción. Usted puede hacerlo por un subconjunto de los valores, es decir, las listas finitas. Pero esto no es lo que [a]es.
Andrej Bauer el