Ich lerne Programmieren in ML (OCaml) und habe früher nach ML-Funktionen vom Typ'a -> 'b
gefragt . Jetzt habe ich ein bisschen mit Funktionen vom Typ experimentiert 'a list -> 'b list
. Es gibt einige offensichtliche einfache Beispiele:
let rec loop l = loop l
let return_empty l = []
let rec loop_if_not_empty = function [] -> []
| l -> loop_if_not_empty l
Was ich nicht herausfinden kann, ist, wie man eine Funktion erstellt, die etwas anderes tut als die leere Liste oder Schleife zurückzugeben (ohne eine Bibliotheksfunktion zu verwenden). Kann das gemacht werden? Gibt es eine Möglichkeit, nicht leere Listen zurückzugeben?
Bearbeiten: Ja, wenn ich eine Funktion vom Typ habe 'a -> 'b
, kann ich eine andere oder eine Funktion vom Typ 'a list -> 'b list
erstellen, aber ich frage mich hier, wie ich die erste erstellen soll.
programming-languages
typing
functional-programming
Gilles 'SO - hör auf böse zu sein'
quelle
quelle
Antworten:
Nun, etwas, das als Parametrizität bekannt ist, sagt uns, dass es, wenn wir die reine Teilmenge von ML betrachten (dh keine unendliche Rekursion
ref
und all das seltsame Zeug), keine andere Möglichkeit gibt, eine Funktion mit diesem Typ zu definieren, als die, die das Leere zurückgibt Liste.Alles begann mit Wadlers Artikel „ Theorems for free! ”. Dieses Papier sagt uns im Grunde zwei Dinge:
ref
und all das seltsame Zeug) erfüllt diese Bedingungen.Aus dem Parametrizität Theorem wissen wir , dass , wenn wir eine Funktion haben
f : 'a list -> 'b list
, dann für alle'a
,'b
,'c
,'d
und für alle Funktioneng : 'a -> 'c
, dieh : 'b -> 'd
wir haben:(Beachten Sie,
f
links hat Typ'a list -> 'b list
undf
rechts ist'c list -> 'd list
.)Wir können frei wählen, was
g
wir wollen, also lassen Sie'a = 'c
undg = id
. Jetzt haben wirmap id = id
(leicht durch Induktion der Definition von zu beweisenmap
):Jetzt lass
'b = 'd = bool
undh = not
. Nehmen wir für einige anzs : bool list
, dass es passiertf zs ≠ [] : bool list
. Es ist klar, dassmap not ∘ f = f
das nicht gilt, weilWenn das erste Element der Liste rechts ist
true
, dann ist links das erste Elementfalse
und umgekehrt!Dies bedeutet, dass unsere Annahme falsch ist und
f zs = []
. Sind wir fertig? Nein.Wir gingen davon aus, dass
'b
istbool
. Wir haben gezeigt , dass , wennf
mit Typ aufgerufen wirdf : 'a list -> bool list
für jede'a
,f
muss immer die leere Liste zurück. Kann es sein, dass wenn wir anrufenf
,f : 'a list -> unit list
es etwas anderes zurückgibt? Unsere Intuition sagt uns, dass dies Unsinn ist: Wir können einfach keine reine ML-Funktion schreiben, die immer die leere Liste zurückgibt, wenn wir möchten, dass sie uns eine Liste von Booleschen Werten gibt, und ansonsten möglicherweise eine nicht leere Liste zurückgibt! Dies ist jedoch kein Beweis.Was wir sagen wollen, ist, dass
f
es einheitlich ist : Wenn es immer die leere Liste für zurückgibtbool list
, muss es die leere Liste fürunit list
und im Allgemeinen für jede zurückgeben'a list
. Genau darum geht es beim zweiten Punkt in der Aufzählungsliste am Anfang meiner Antwort.Das Papier sagt uns , dass in ML
f
nehmen muß damit verbundene Werte zu verwandt denjenigen. Ich werde nicht in die Details über die Beziehungen, ist es genug , um zu sagen , dass Listen werden im Zusammenhang , wenn und nur wenn sie die gleiche Länge haben und ihre Elemente sind paarweise im Zusammenhang (das heißt,[x_1, x_2, ..., x_m]
und[y_1, y_2, ..., y_n]
beziehen sich, wenn und nur wennm = n
undx_1
bezieht sich aufy_1
undx_2
ist verwandt mity_2
und so weiter). Und der Spaß daran ist, in unserem Fall, daf
polymorph ist, wir können definieren , jede Beziehung auf die Elemente von Listen!Lassen Sie uns holen jeder
'a
,'b
und schauen Sie sichf : 'a list -> 'b list
. Nun sieh dir anf : 'a list -> bool list
; Wir haben bereits gezeigt, dass in diesem Fallf
immer die leere Liste zurückgegeben wird. Wir postulieren nun, dass alle Elemente von'a
sich auf sich selbst beziehen (denken Sie daran, wir können jede gewünschte Beziehung wählen), dies impliziert, dass sich jedezs : 'a list
auf sich selbst bezieht. Wie wir wissen, werdenf
verwandte Werte mit verwandten Werten in Verbindung gebracht. Dies bedeutet, dass sief zs : 'b list
verwandt sindf zs : bool list
, aber die zweite Liste hat eine Länge von Null, und da die erste Liste damit verwandt ist, ist sie auch leer.Der Vollständigkeit halber möchte ich erwähnen, dass es in der Originalarbeit des Wadlers einen Abschnitt über die Auswirkungen der allgemeinen Rekursion (mögliche Nichtbeendigung) gibt, und es gibt auch eine Arbeit , die freie Theoreme in Gegenwart von untersucht
seq
.quelle
g
h
Kehren wir zu einfacheren Objekten zurück: Sie können kein geeignetes Objekt vom Typ erstellen,
'a
da dies bedeuten würde, dass dieses Objektx
überall dort verwendet werden kann, wo'a
es passt. Und das heißt überall: als Ganzzahl, als Array, sogar als Funktion. Zum Beispiel , das würde bedeuten , man Dinge tun kann , wiex+2
,x.(1)
und(x 5)
. Typen existieren genau , um dies zu verhindern.Dies ist die gleiche Idee, die für eine Funktion vom Typ gilt
'a -> 'b
, aber es gibt einige Fälle, in denen dieser Typ existieren kann: Wenn die Funktion niemals ein Objekt vom Typ zurückgibt'b
: Wenn eine Ausnahme wiederholt oder ausgelöst wird.Dies gilt auch für Funktionen, die eine Liste zurückgeben. Wenn Ihre Funktion vom Typ ist
t -> 'b list
und Sie ein Objekt vom Typ erstellent
und auf diese Funktion anwenden, bedeutet dies, dass Sie bei erfolgreichem Zugriff auf ein Element dieser Liste auf ein Objekt mit allen Typen zugreifen. Sie können also auf kein Element der Liste zugreifen: Die Liste ist entweder leer oder ... es gibt keine Liste.Der Typ
'a list -> 'b list
erscheint jedoch in üblichen Übungen, aber das ist nur, wenn Sie bereits eine Funktion des Typs haben'a -> 'b
:Aber Sie kennen diesen wahrscheinlich.
quelle
'a -> 'b
oder ist'a list -> 'b list
, aber das ist keine so interessante Beobachtung. Tatsächlich werde ich die Frage bearbeiten, um klar zu machen, dass dies nicht das ist, worüber sich der jüngere Schüler beim Programmieren Gedanken gemacht hat.f : 'a list -> 'b list
und einet
solche erzeugen können ,f t <> []
wird dieses Programm die Typprüfung durchführen, kann jedoch weitaus schlechter abschneiden als das Auslösen einer Ausnahme :let y = List.hd (f t) in (y y) (y + y.(0) + y.(0).(0))
.Parametrizitätssatz aus den "Theorems for Free!" Das Papier sagt uns, dass ML-Begriffe eine ganz besondere Eigenschaft haben: Wenn wir den Typ eines Begriffs als Beziehung zu Werten dieses Typs betrachten, wird der Wert dieses Begriffs mit sich selbst in Beziehung gesetzt. So sehen Sie Typen als Beziehungen an:
'a -> 'b
entspricht der Beziehung, die definiert wird, indem gesagt wird, dass zwei Funktionen verwandt sind, wenn sie verwandte Werte mit verwandten Werten annehmen (vorausgesetzt'a
und'b
einigen Beziehungen entsprechen).'a list
entspricht der Beziehung, die definiert wird, indem gesagt wird, dass zwei Listen miteinander verbunden sind, wenn sie dieselbe Länge haben und ihre übereinstimmenden Elemente miteinander verbunden sind (vorausgesetzt, dies'a
entspricht einer Beziehung).foo : 'a -> 'a
foo
oder mit anderen Worten:
Das ist genau der freie Satz für die
id
Funktion :f . id = id . f
.foo : 'a list -> 'b list
Jetzt verwenden wir dies, um zu beweisen, dass für zwei beliebige Typen
A
undB
die Funktionfoo
eine leere Liste für jede Eingabe zurückgibtas : A list
.A
Ø
B
as
ist mit sich selbst verwandt (wie wir die Identitätsbeziehung gewählt habenA
), ist alsofoo as : Ø list
verwandt mitfoo as : B list
.Ø
Typs geben kann.Daher muss für jeden
A
,B
undas : A list
wir haben,foo as : B list
das muss eine leere Liste sein.quelle