Quel point fixe est le type de liste Haskell?

9

Disons que les listes sont définies comme

List a = Nil | Cons a (List a)

Alors, à Haskell est List xle plus grand point ou le moins fixe? Je demande parce que le lfp devrait exclure les listes infinies (mais vous pouvez les construire dans Haskell), tandis que le gfp devrait exclure les listes finies.

programming-languages type-theory functional-programming semantics category-theory miniBill
la source

Réponses:

4

La bonne chose est de configurer

data ListF a x = Nil | Cons a x

Vous pouvez maintenant écrire

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

À Haskell, nous pouvons observer cela Mu ListFet Nu ListFcoïncider. Donc, ça peut être soit (!). (une source sur cette demande: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf )

De plus, nous pouvons prouver les choses par induction sur toutes les listes et obtenir des preuves qui fonctionnent tant que nous nous limitons à nous préoccuper des finis, comme décrit ici: http://www.cs.ox.ac.uk/jeremy.gibbons/ publications / fast + loose.pdf

Deux autres références à ce sujet sont:

sclv
la source
Je pense que vous manquez un x dans cette déclaration de type de données ...
miniBill
2
Il y a une raison pour laquelle Jeremy a qualifié ce papier de "rapide et lâche". Cette réponse est exactement le genre de déni dont je parle. C'est le plus grand point fixe, la fin de l'histoire. Le premier article lié de Jeremy en parle, par exemple.
Andrej Bauer
10

C'est le plus grand point fixe, ou la dernière hébreu, selon la façon dont vous configurez les choses. Dans Haskell, il est impossible de définir le type de données des listes finies car Haskell n'a pas de types inductifs, seulement les types coinductifs. Beaucoup de gens nient ce problème particulier.

Andrej Bauer
la source
Beaucoup de gens sont dans le déni?
miniBill
2
Bien sûr, je rencontre des gens qui essaient de prouver les choses par induction sur des listes, des arbres, etc. à Haskell. Ils prétendent que tous ces types de données sont inductifs.
Andrej Bauer
Et vous ne pouvez pas prouver les choses par induction sur des listes?
miniBill
2
Vous ne pouvez pas prouver les propriétés du type [a]dans Haskell par induction. Vous pouvez le faire pour un sous-ensemble des valeurs, à savoir les listes finies. Mais ce n'est pas ce qui [a]est.
Andrej Bauer