Warum akzeptiert Haskell meine kombinatorische "Zip" Definition nicht?

8

Dies ist die Textbuch-Zip-Funktion:

%Vor%

Ich fragte auf #haskell früher, ob "zip" mit "foldr" alleine implementiert werden könnte, keine Rekursion, kein Mustervergleich. Nach einigem Nachdenken stellten wir fest, dass die Rekursion durch Fortsetzungen eliminiert werden konnte:

%Vor%

Uns bleibt immer noch die Mustererkennung. Nach etwas mehr Neuronentoasting kam ich zu einer unvollständigen Antwort, die ich für logisch hielt:

%Vor%

Es gibt eine flache Liste zurück, aber das Zippen wird ausgeführt. Ich war sicher, dass es einen Sinn ergab, aber Haskell beklagte sich über den Typ. Ich fuhr fort, es auf einem untypisierten Lambda-Rechner zu testen, und es funktionierte. Warum kann Haskell meine Funktion nicht akzeptieren?

Der Fehler ist:

%Vor%     
MaiaVictor 26.04.2015, 15:59
quelle

3 Antworten

6

Warum Ihre Definition nicht akzeptiert wird: Sehen Sie sich das an:

%Vor%

Wenn Sie also die erste Funktion als Argument für foldr verwenden möchten, erhalten Sie (wenn Sie die Typen von foldr s zuerst Argument angeben:

) %Vor%

was natürlich ein Problem ist (als r und (r -> [a]) -> [a] wechselseitig rekursiv und sollten beide gleich b' sein)

Das sagt Ihnen der Compiler

wie man es repariert

Sie können Ihre Idee mit

reparieren %Vor%

was ich ausgeliehen habe original Verwenden Sie .

Mit diesem können Sie schreiben:

%Vor%

und du bekommst:

%Vor%

was (was ich denke) du wolltest.

ABER Offensichtlich müssen beide Listen von demselben Typ sein, also weiß ich nicht, ob Ihnen das wirklich helfen wird

    
Carsten 26.04.2015, 16:30
quelle
2

Wir können den expliziten Mustervergleich eliminieren, indem wir eine Funktion definieren, die dies für uns tun wird.

Betrügt es? Nicht, wenn maybe und bool sind erlaubt, so wie sie sind; Dann sollten wir auch list zulassen,

%Vor%

genauso; damit wir in Ihrer zip' -Definition

haben können %Vor%

oder z.B.

%Vor%

wenn Sie diese Art von Sache bevorzugen.

Über Ihren Fehler gibt "unendlicher Typ" häufig Selbstanwendung an; In der Tat, was auch immer Ihr zipper zurückgibt, Sie wenden es selbst an, in Ihrem

%Vor%

Ich habe versucht, Ihre Definition zu optimieren und kam mit

%Vor%

Es scheint sich auf dem Papier korrekt zu reduzieren, aber ich habe auch hier die unendlichen Typfehler.

Es gibt jetzt keine (augenscheinliche) Selbstanwendung, aber der Typ der Fortsetzung, den die erste Zip-Datei erhält, hängt vom Typ der ersten Zip-Datei selbst ab; Es gibt also immer noch eine zirkuläre Abhängigkeit: tq ist auf beiden Seiten der Typ-Äquivalenz in tq ~ a -> tr -> [(a,b)] ~ a -> (tq -> [(a,b)]) -> [(a,b)] .

Tatsächlich sind das die zwei Typfehler, die ich bekomme (der erste betrifft den tr -Typ),

%Vor%

In den üblichen Definitionen, die foldr mit Fortsetzungen verwenden, ist der Typ dieser Fortsetzungen unabhängig; das ist der Grund, dass es dort funktioniert, denke ich.

    
Will Ness 26.04.2015 23:38
quelle
2

Ich kann Ihnen eine etwas andere Perspektive bieten (denke ich), um zu einer ähnlichen Lösung wie Carstens (aber mit einfacheren Typen) zu kommen.

Hier ist wieder dein Code, für deine "weben zip" (Ich schreibe tr für "die Art von r ", ähnlich tq für "die Art von q "; ich benutze immer " r "für das rekursive Ergebnis Argument der Kombinationsfunktion in foldr Definitionen, als mnemotechnisches Gerät):

%Vor%

Also, das ist der unendliche Typ. Haskell erlaubt dies nicht für einen beliebigen Typ (für welchen Typ Variablen stehen).

Aber Haskells Datentypen lassen tatsächlich eine Rekursion zu. Listen, Bäume usw. - alle üblichen Typen sind rekursiv. Dieses ist erlaubt:

%Vor%

Hier haben wir tun denselben Typ auf beiden Seiten der Gleichung, genauso wie wir tr auf beiden Seiten der Typäquivalenz tr ~ tr -> [a] haben. Aber es ist ein spezifischer Typ, kein willkürlicher.

Also deklarieren wir es einfach, indem wir der obigen "Gleichung" folgen:

%Vor%

Was ist ein Tree a Typ? Es ist "etwas", das in ein Branch geht, was ein Tree a ist. Ein gegebener Baum muss nicht unendlich konstruiert sein, weil undefined auch den Typ Tree a hat.

Was ist ein TR a Typ? Es ist "etwas" in TR a -> [a] , was ein TR a ist. Ein gegebenes TR a muss nicht unendlich konstruiert sein, weil const [] auch vom Typ TR a sein kann.

Unser Möchtegern-Rekursivtyp tr ~ tr -> [a] wurde zu einer echten rekursiven Typdefinition newtype TR a = Pack { TR a -> [a] } , die sich hinter dem Datenkonstruktor Pack versteckt (was der Compiler dank des verwendeten newtype -Schlüsselwortes loswerden wird) , aber das ist ein überflüssiges Detail, es funktioniert auch mit data ).

Haskell behandelt hier die Rekursivität. Typentheoretiker lieben es, sich selbst damit zu befassen, mit Fix und whatnot; aber ein Haskell-Benutzer hat dies bereits in der Sprache verfügbar. Wir müssen nicht verstehen, wie es implementiert ist, um es nutzen zu können. Wir müssen das Rad nicht neu erfinden, bis wir es selbst bauen wollen.

Also, zipper xs hatte den Typ tr ; jetzt wird es TR a , also muss das neue zipper xs zurückkehren - die "gepackte" Listenerstellungsfunktion. Die Kombinationsfunktion foldr muss den Wert zurückgeben, den der Aufruf zipper zurückgibt (nach den Tugenden von foldr definition). Um die gepackte Funktion anzuwenden, müssen wir nun unpack es zuerst:

%Vor%     
Will Ness 29.04.2015 13:07
quelle

Tags und Links