Welcher Fixpunkt ist der Haskell-Listentyp?

9

Angenommen, Listen sind definiert als

List a = Nil | Cons a (List a)

Dann ist in Haskell List xder größte oder kleinste Fixpunkt? Ich frage, weil das lfp unendliche Listen ausschließen sollte (aber Sie können sie in Haskell erstellen), während das gfp endliche ausschließen sollte.

miniBill
quelle

Antworten:

4

Das Richtige ist das Setup

data ListF a x = Nil | Cons a x

Jetzt kannst du schreiben

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

In Haskell können wir das beobachten Mu ListFund Nu ListFzusammenfallen. Es kann also entweder (!) Sein. (Eine Quelle zu dieser Behauptung: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf )

Darüber hinaus können wir Dinge durch Induktion auf allen Listen beweisen und Beweise erhalten, die funktionieren, solange wir uns darauf beschränken, uns um endliche zu kümmern, wie hier beschrieben: http://www.cs.ox.ac.uk/jeremy.gibbons/ Veröffentlichungen / fast + lose.pdf

Zwei weitere Referenzen hierzu sind:

sclv
quelle
Ich denke, Sie vermissen ein x in dieser Datentypdeklaration ...
miniBill
2
Es gibt einen Grund, warum Jeremy dieses Papier "schnell und locker" nannte. Diese Antwort ist genau die Art von Ablehnung, von der ich spreche. Es ist der größte Fixpunkt, das Ende der Geschichte. In Jeremys erstem verlinkten Artikel geht es zum Beispiel darum.
Andrej Bauer
10

Es ist der größte Fixpunkt oder die endgültige Kohlegebra, je nachdem, wie Sie die Dinge einrichten. In Haskell ist es unmöglich, den Datentyp endlicher Listen zu definieren, da Haskell keine induktiven Typen hat, sondern nur die koinduktiven. Viele Menschen leugnen dieses spezielle Problem.

Andrej Bauer
quelle
Viele Menschen leugnen?
MiniBill
2
Klar, ich treffe Leute in Haskell, die versuchen, Dinge durch Induktion auf Listen, Bäumen usw. zu beweisen. Sie geben vor, dass alle diese Datentypen induktiv sind.
Andrej Bauer
Und Sie können Dinge nicht durch Induktion auf Listen beweisen?
MiniBill
2
Sie können Eigenschaften des Typs [a]in Haskell nicht durch Induktion nachweisen. Sie können dies für eine Teilmenge der Werte tun, nämlich für die endlichen Listen. Aber das ist nicht was [a]ist.
Andrej Bauer