Calculus und Maclaurin-Reihen mit Typen
Hier noch ein kleiner Zusatz - ein kombinatorischer Einblick in die Frage, warum die Koeffizienten in einer Reihenentwicklung "funktionieren" sollten, wobei der Schwerpunkt auf Reihen liegt, die sich mit Hilfe der Taylor-Maclaurin Ansatz aus dem Kalkül. NB: Die von Ihnen genannte Beispielserienerweiterung des Typs "manipulierte Liste" ist eine Maclaurin-Reihe.
Da sich andere Antworten und Kommentare mit dem Verhalten von algebraischen Ausdrücken (Summen, Produkte und Exponenten) befassen, wird in dieser Antwort auf dieses Detail verzichtet und der Schwerpunkt auf den Typ "Kalkül" gelegt.
Sie werden feststellen, dass Anführungszeichen in dieser Antwort eine wichtige Rolle spielen. Dafür gibt es zwei Gründe:
- es geht darum, Entitäten aus einem anderen Bereich zu interpretieren, und es scheint angemessen, solche Fremdbegriffe auf diese Weise abzugrenzen.
- Einige Begriffe können strenger formalisiert werden, aber die Form und die Ideen scheinen wichtiger zu sein (und benötigen weniger Platz zum Schreiben) als die Details.
Definition der Maclaurin-Reihe
En Maclaurin-Reihe einer Funktion f : ist definiert als
f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f(0)X + ...
何所 f bedeutet die n th Ableitung von f .
Um die Maclaurin-Reihe bei der Interpretation mit Typen verstehen zu können, müssen wir verstehen, wie wir drei Dinge in einem Typenkontext interpretieren können:
- eine (möglicherweise mehrfache) Ableitung
- Anwendung einer Funktion auf
0
- Begriffe wie
(1/n!)
und es stellt sich heraus, dass diese Konzepte aus der Analyse passende Entsprechungen in der Welt der Schrift haben.
Was verstehe ich unter einem "geeigneten Gegenstück"? Es sollte den Geschmack eines Isomorphismus haben - wenn wir die Wahrheit in beiden Richtungen bewahren können, können Fakten, die in einem Kontext ableitbar sind, auf den anderen übertragen werden.
Kalkül mit Typen
Was bedeutet also die Ableitung eines Typenausdrucks? Es stellt sich heraus, dass es für eine große und wohlbehaltene ("differenzierbare") Klasse von Typausdrücken und Funktoren eine natürliche Operation gibt, die sich ähnlich genug verhält, um eine geeignete Interpretation zu sein!
Um die Pointe zu verderben: Die Operation, die der Differenzierung entspricht, ist die Herstellung von "Ein-Loch-Zusammenhängen". Diese ist ein hervorragender Ort, um diesen Punkt weiter zu vertiefen, aber das Grundkonzept eines Ein-Loch-Kontextes ( da/dx ) ist, dass er das Ergebnis der Extraktion eines einzelnen Untereintrags eines bestimmten Typs ( x ) aus einem Begriff (vom Typ a ), wobei alle anderen Informationen, einschließlich derjenigen, die zur Bestimmung des ursprünglichen Standorts des Unterpostens erforderlich sind, erhalten bleiben. Eine Möglichkeit, einen Ein-Loch-Kontext für eine Liste darzustellen, sind beispielsweise zwei Listen: eine für die Elemente, die vor dem extrahierten Element lagen, und eine für die Elemente, die danach kamen.
Die Motivation für die Identifizierung dieses Vorgangs mit der Differenzierung ergibt sich aus den folgenden Beobachtungen. Wir schreiben da/dx den Typ der Ein-Loch-Kontexte für den Typ a mit Loch vom Typ x .
d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx
Hier, 1 et 0 stehen für Typen mit genau einem bzw. genau null Einwohnern, und + et × wie üblich Summe und Produkttypen darstellen. f et g werden verwendet, um Typfunktionen oder Typausdruckserzeuger darzustellen, und [f(x)/a] ist der Vorgang der Ersetzung f(x) für jeden a im vorhergehenden Ausdruck.
Dies kann in einem punktfreien Stil geschrieben werden, indem man f' die Ableitungsfunktion vom Typ Funktion f also:
(x 1)' = x 0
(x x)' = x 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g f)' = (g' f) × f'
was möglicherweise vorzuziehen ist.
NB: Die Gleichheiten können rigoros und exakt gemacht werden, wenn wir Ableitungen unter Verwendung von Isomorphieklassen von Typen und Funktoren definieren.
Nun stellen wir fest, dass die Regeln der Infinitesimalrechnung für die algebraischen Operationen der Addition, Multiplikation und Komposition (oft als Summen-, Produkt- und Kettenregeln bezeichnet) genau durch die Operation des "Löcherns" wiedergegeben werden. Außerdem sind die Grundfälle des "Löcherns" in einem konstanten Ausdruck oder dem Term x selbst verhalten sich auch wie Differenzierung, so dass wir durch Induktion ein differenzierungsähnliches Verhalten für alle algebraischen Ausdrücke erhalten.
Jetzt können wir die Differenzierung interpretieren, was bedeutet die n die 'Ableitung' eines Typausdrucks, de/dx bedeuten? Es handelt sich um einen Typ, der n -Ortskontexte: Begriffe, die, wenn sie "gefüllt" werden mit n Bezeichnungen der Art x einbringen e . Es gibt eine weitere wichtige Beobachtung in Bezug auf (1/n!) ' kommt später.
Der invariante Teil eines Typ-Funktors: Anwendung einer Funktion auf 0
Wir haben bereits eine Interpretation für 0 in der Welt der Typen: ein leerer Typ ohne Mitglieder. Was bedeutet es aus kombinatorischer Sicht, eine Typfunktion auf ihn anzuwenden? Konkreter ausgedrückt, nehmen wir an f eine Typfunktion ist, was bedeutet f(0) aussehen? Nun, wir haben sicherlich keinen Zugang zu irgendetwas von der Art 0 so dass alle Konstruktionen von f(x) die eine x sind nicht verfügbar. Was übrig bleibt, sind die Begriffe, die in ihrer Abwesenheit zugänglich sind, was wir den "invarianten" oder "konstanten" Teil des Typs nennen können.
Ein explizites Beispiel hierfür ist die Maybe Funktor, der algebraisch dargestellt werden kann als x 1 + x . Wenn wir dies anwenden auf 0 erhalten wir 1 + 0 - es ist einfach wie 1 : der einzig mögliche Wert ist der None Wert. Bei einer Liste erhalten wir ebenfalls nur den Begriff, der der leeren Liste entspricht.
Wenn wir sie zurückbringen und den Typ interpretieren f(0) als Zahl kann man sie sich als die zählen wie viele Begriffe des Typs f(x) (für jede x ) kann ohne Zugang zu einer x : das heißt, die Anzahl der "leerähnlichen" Begriffe.
Zusammenstellung: Vollständige Interpretation einer Maclaurin-Serie
Ich fürchte, mir fällt keine angemessene direkte Interpretation von (1/n!) als Typ.
Wenn wir jedoch den Typ f(0) In Anbetracht der obigen Ausführungen lässt sich feststellen, dass sie als die Art der n -Platzkontexte für einen Begriff des Typs f(x) die enthalten nicht bereits eine x - das heißt, wenn wir sie "integrieren n mal, hat der resultierende Begriff genau n x s, nicht mehr und nicht weniger. Dann ist die Interpretation des Typs f(0) als eine Zahl (wie die Koeffizienten der Maclaurin-Reihe von f ) ist einfach eine Zählung, wie viele solcher leeren n -Platz-Kontexte gibt. Wir sind fast am Ziel!
Aber wo ist (1/n!) enden? Die Untersuchung des Prozesses der "Differenzierung" des Typs zeigt uns, dass bei mehrfacher Anwendung die "Reihenfolge", in der die Unterbegriffe extrahiert werden, erhalten bleibt. Betrachten wir zum Beispiel den Begriff (x, x) vom Typ x × x und den Vorgang des "Löcherns" zweimal. Wir erhalten beide Sequenzen
(x, x) (_, x) (_, _)
(x, x) (x, _) (_, _)
(where _ represents a 'hole')
obwohl beide von demselben Begriff stammen, denn es gibt 2! = 2/code> ways to take two elements from two, preserving order. In general, [there are `n!`](https://en.m.wikipedia.org/wiki/Permutation) ways to take `n` elements from `n`. So in order to get a count of the number of configurations of a functor type which have `n` elements, we have to count the type `f(0)` and divide by `n!`, _exactly_ as in the coefficients of the Maclaurin series.
``
So dividing by n! turns out to be interpretable simply as itself.
Final thoughts: 'recursive' definitions and analyticity
First, some observations:
- if a function f : has a derivative, this derivative is unique
- similarly, if a function f : is analytic, it has exactly one corresponding polynomial series
Since we have the chain rule, we can use implicit differentiation, if we formalise type derivatives as isomorphism classes. But implicit differentiation doesn't require any alien manoeuvres like subtraction or division! So we can use it to analyse recursive type definitions. To take your list example, we have
L(X) 1 + X × L(X)
L'(X) = X × L'(X) + L(X)
and then we can evaluate
L'(0) = L(0) = 1
to obtain the coefficient of X¹ in the Maclaurin series.
But since we are confident that these expressions are indeed strictly 'differentiable', if only implicitly, and since we have the correspondence with functions , where derivatives are certainly unique, we can rest assured that even if we obtain the values using 'illegal' operations, the result is valid.
Now, similarly, to use the second observation, due to the correspondence (is it a homomorphism?) with functions , we know that, provided we are satisfied that a function has a Maclaurin series, if we can find any series at all, the principles outlined above can be applied to make it rigorous.
As for your question about composition of functions, I suppose the chain rule provides a partial answer.
I'm not certain how many Haskell-style ADTs this applies to, but I suspect it is many if not all. I have discovered a truly marvellous proof of this fact, but this margin is too small to contain it...
Now, certainly this is only one way to work out what is going on here and there are probably many other ways.
Summary: TL;DR
- type 'differentiation' corresponds to 'making a hole'.
- applying a functor to
0 gets us the 'empty-like' terms for that functor.
- Maclaurin power series therefore (somewhat) rigorously correspond to enumerating the number of members of a functor type with a certain number of elements.
- implicit differentiation makes this more watertight.
- uniqueness of derivatives and uniqueness of power series mean we can fudge the details and it works.
``
