Qual ponto de correção é o tipo de lista Haskell?

Digamos que as listas sejam definidas como

List a = Nil | Cons a (List a)

Então, em Haskell, List xo maior ou o menos fixo? Estou perguntando porque o lfp deve excluir listas infinitas (mas você pode construí-las em Haskell), enquanto o gfp deve excluir as finitas.

O certo é configurar

data ListF a x = Nil | Cons a x

Agora você pode escrever

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

Em Haskell, podemos observar isso Mu ListFe Nu ListFcoincidir. Então, pode ser (!). (uma fonte sobre essa reivindicação: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf )

Além disso, podemos provar as coisas por indução em todas as listas e obter provas que funcionem desde que nos limitemos a cuidar de questões finitas, conforme descrito aqui: http://www.cs.ox.ac.uk/jeremy.gibbons/ publicações / fast + loose.pdf

Duas outras referências sobre isso são:

• http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt (que é um documento historicamente crucial)

• http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.1418 (que é uma excelente exposição)

É o melhor ponto fixo, ou a coalgebra final, dependendo de como você define as coisas. Em Haskell, é impossível definir o tipo de dados das listas finitas, porque Haskell não possui tipos indutivos, apenas os coindutivos. Muitas pessoas estão negando esse problema em particular.