Was sind unendliche Typen?

Question

Offenbar gibt es in Haskell etwas genannt unendlich Typ.

Zum Beispiel, wenn ich iterate concat auf GHCi versuchen, bekomme ich diese:

*Main> iterate concat 

<interactive>:24:9: error: 
    • Occurs check: cannot construct the infinite type: a ~ [a] 
     Expected type: [a] -> [a] 
     Actual type: [[a]] -> [a] 
    • In the first argument of ‘iterate’, namely ‘concat’ 
     In the expression: iterate concat 
     In an equation for ‘it’: it = iterate concat 
    • Relevant bindings include 
     it :: [a] -> [[a]] (bound at <interactive>:24:1) 

Meine Frage ist, was genau sind unendlich Typen? Wie passen sie in die Typentheorie und aus welchen Quellen kann ich etwas über sie lernen? Gibt es Programmiersprachen, die unendliche Arten erlauben?

Answer 1

Anscheinend gibt es in Haskell etwas, das als unendlicher Typ bezeichnet wird.

Da die Haskell Typ-Checker einen Typfehler wirft jedes Mal eine unendliche Art entstehen würde, würde ich sagen, es gibt keine unendliche Arten in Haskell.

Wie auch immer, "unendliche" Typen beziehen sich darauf, wie viele Typkonstruktoren im Typ selbst erscheinen. Zum Beispiel erwähnt [], Bool, Int, (->), so ist es endlich. Wenn wir type L = [[[[...]]]] mit unendlich vielen Verschachtelungen schreiben könnten, hätten wir einen unendlichen Typ: einen Typ, dessen Werte Listen von Listen von Listen sind ... für immer.

Unendliche Typen können durch Vereinheitlichung während der Typinferenz entstehen. Wenn ich

schreiben

let x = [x] in ... 

dann, wenn T die Art der x ist, muss es auch die Art der [x] per Definition sein. Letztere hat jedoch eindeutig den Typ [T]. Daher müssen wir die Gleichung T = [T] lösen, deren Lösung zu dem oben diskutierten unendlichen Typ L führen würde.

Haskell lehnt, wie praktisch alle Programmiersprachen, unendliche Typen ab, da sie oft Symptome eines Programmierfehlers sind. Außerdem denke ich, dass das Hinzufügen endloser (regulärer) Typen die Typprüfung erheblich erschweren kann. Ich kann mich an kein theoretisches Ergebnis über unendliche Typen erinnern, aber ich wäre nicht überrascht, wenn die Typprüfung unentscheidbar würde.

Answer 2

"Unendlich" -Typen sind nicht wirklich Teil der Typentheorie. Im Allgemeinen hält sich Math von Dingen fern, die "für immer weitergehen". Formal suchen Sie nach dem Begriff rekursive Typen. Die meisten Programmiersprachen do unterstützen rekursive Typen, aber nur wenn sie von einem zusätzlichen Konstruktor geschützt werden. In Haskell, zum Beispiel wird die folgende erlaubt (in der Tat, zur Laufzeit, würde es zu einer unendlich verschachtelten Liste in ihrer Darstellung äquivalent):

newtype InfinitelyNestedList a = Nest [InfinitelyNestedList a] 

Jedoch gibt ist eine Formalisierung dieser Art von was genau das ist worüber du geredet hast: equirecursive "mu" types (das sollte dir einen guten Startpunkt geben). Das Mischen der Liste Typkonstruktor in, können Sie die unendlich verschachtelten Liste Typ denken als

µ x. [x] 

Keine große populäre Sprache, die ich von Verwendungen kennen Arten equirecursive und das aus gutem Grund - es bedeutet, dass Sie nicht mehr einen Haupttyp haben. In Haskell kann jeder Typ normalisiert werden. Wenn Sie also prüfen wollen, ob zwei Typen gleich sind (im Compiler), normalisieren Sie sie und vergleichen Sie sie. Hier jedoch verlierst du das. Zum Beispiel sind die folgenden Typen alle völlig gleich!

µ x. [x] 
[[µ x. [x]]] 
[[[[[[[µ x. [x]]]]]]]] 

In diesem Fall normalisieren die Compiler könnten zusätzlich auf den „einfachste“ ersten Fall - aber im Allgemeinen gibt es keinen Begriff der „einfachste“.

Answer 3

"Unendlich Arten" sind nicht wirklich eine spezielle Sache, so weit ich weiß. Ich las diese Zeile der Fehlermeldung:

Occurs check: cannot construct the infinite type: a ~ [a] 

nur als „unendlich“ als Adjektiv mit einem Typ zu beschreiben, nicht „unendlich Typen“ als Name für eine spezielle Klasse von Typ verwendet wird. Der Compiler erkannte, dass ein Typ benötigt wird, der a ~ [a] erfüllt, um Ihrem Code einen Typ zu geben, und er kann einen solchen Typ nicht verarbeiten.

Die Fehlermeldung wäre völlig richtig, wenn es gerade ist:

Occurs check: cannot construct the type: a ~ [a] 

Das Wort unendlich hinzugefügt werden nur zu markieren, was das Problem ist. Wenn der Typ a mit [a] vereinheitlicht, dann vereinheitlicht es auch mit [[a]], [[[a]]], usw. Es wird nie mit einem Listentyp eine endliche Anzahl verschachtelt vereinigen, da es a ~ [a] noch einmal erweitern kann.