Gibt es „Logarithmustypen“?

Question

Ich versuche, einige meiner Gedanken zu Pfaden in Datenstrukturen zu formalisieren.Zum Beispiel ein Pfad in eine Liste von Ts könnte ein Paar aus einem Index und einem Pfad in a sein T;ein Weg in ein Paar (A, B) wäre die getaggte Vereinigung eines Pfades hinein A oder ein Weg hinein B.Stellen Sie sich einen Pfad als eine Möglichkeit vor, einen kleinen (atomaren?) Teil einer größeren Datenstruktur anzugeben – nicht unähnlich einer Linse, aber hier betone ich die strukturelle Zerlegung eines Datentyps im Gegensatz zu einer willkürlichen Berechnung, die die Linse erfüllt Gesetze (vielleicht ist jeder Weg als Linse verwendbar, aber nicht jede Linse entspricht einem Weg).

Genau genommen mein erstes Beispiel über Listen von Ts ist ein wenig schlampig, da ein Pfad in eine solche Liste führt l Der Index sollte durch die Länge von begrenzt sein l.Das Paar (Nat, path T) ist eigentlich ein Weg in einen unendlich Liste von Ts – oder gleichbedeutend ein Pfad in eine Funktion Nat -> T.

Meine erste interessante Beobachtung ist also, dass ich einen Operator habe, der Exponentialzahlen in Produkte und Produkte in Summen umwandelt, und zwar auf eine Weise, die furchtbar an Logarithmen erinnert:

path (T^Nat) = Nat * (path T)
path (A * B) = path A + path B

Das brachte mich dazu, darüber nachzudenken, ob es eine gibt exp T Typ auch.Abgesehen von aller Zurückhaltung und Strenge gelten die Bedingungen der üblichen Serienerweiterung für $e^x$ einen Hinweis geben:

$$e^x = \sum_{n\ge0} \frac {x^n} {n!}$$

Eine typtheoretische Interpretation von $\frac {x^n} {n!}$ könnte eine Tüte (wie im Multiset) sein $x$s der Größe $n$ (es ist ein $n$-Tupel $x^n$ aber das ist uns egal $n!$ wie das Tupel geordnet werden kann), also dann ein Wert vom Typ $e^x$ wäre eine Tüte davon $x$s jeder Größe.

Also wenn bag Und path könnte invers sein, dann heißt das so etwas wie der Typ aller Pfade in einen Typ T, falls vorhanden, ist isomorph zu T.Es gibt zum Beispiel einen offensichtlichen Isomorphismus zwischen (bag A) * (bag B) Und bag (A + B) (ein Isomorphismus, der beim Ersetzen nicht funktioniert bag mit list oder set oder eine andere Sammlungsart, was meine Intuition bestärkt bag ist die richtige Interpretation von $e^x$).

Das ist natürlich alles verlockend klingender Unsinn.Ich habe noch nicht einmal formal definiert, was ein Pfad ist Ist, ganz zu schweigen von all den Missbräuchen, die mit der Vortäuschung der Serienerweiterung von verbunden sind $e^x$ ist ein algebraischer Datentyp. path kann auch eine Idee von begrenztem Nutzen sein, da mir überhaupt nicht klar ist, was ich von so etwas halten soll path (A + B) oder path Bool.Aber hat jemand diese Ideen genauer untersucht?Suche nach „Typentheorie“ oder „algebraische Datentypen“ zusammen mit „Logarithmen“, „Pfaden“, „Taschen“, „Multimengen“ usw.hat noch nichts ergeben, was ich hier zu beschreiben versuche.

Answer 1

Logarithmustypen sind definitiv eine Sache und wurden bereits von einer Reihe von Menschen bemerkt.In der funktionalen Programmierung a Type -> Type Der Funktor hat einen Logarithmus, wenn ja darstellbar, und dann ist der Logarithmus das darstellende Objekt.Siehe auch Das, Das, Und Das.Sie haben Recht damit, dass der Exponentialfunktor der Taschenfunktor ist, siehe z. B. Das, wo es als Fixpunkt des beschrieben wird Derivat Operation an Endofunktoren.

Answer 2

Neben der Antwort von András gibt es noch eine Sache, die Sie bei all dem beachten sollten.Ich denke, es ist nicht sehr bekannt, denn obwohl es mir schon vor vielen Jahren aufgefallen ist, habe ich nicht wirklich mit vielen Leuten darüber gesprochen.

Wenn Sie über eine endliche Arithmetik hinter der Arithmetik von Typen nachdenken und sie mit einigen Potenzreihenformeltypen vergleichen, wird das, was Sie erhalten, im Grunde genommen keinen Sinn ergeben.Beispielsweise werden Sie wahrscheinlich auf die booleschen Werte stoßen, die als geschrieben werden $\mathbf 2$, weil es zwei Werte hat.Wenn Sie nun die Formel für ungeordnete Paare aufschreiben, sagen Sie: $$\frac{2^2}{2!} = 2$$ und erwarten Sie, dass die ungeordneten Paare von Booleschen Werten isomorph zu den Booleschen Werten sind.Aber das ist eigentlich falsch;Es gibt drei ungeordnete Paare: $$\{0,0\}, \{0,1\}, \{1,1\}$$

Der Grund dafür ist, dass wir bei der Arbeit mit tatsächlichen Typen entweder die relevanten Permutationen überzählen oder einige der Werte relativ zu ihrer Darstellung in Form kombinatorischer Arten zu wenig zählen.Was die Permutationen betrifft, gibt es eine Permutation dazwischen $(0,1)$ Und $(1,0)$, Aber $(0,0)$ Und $(1,1)$ können nicht in verschiedene geordnete Paare permutiert werden.Was die Werte betrifft, gibt es sie tatsächlich zwei Möglichkeiten, wie wir uns eine Darstellung vorstellen können $(0,0)$ in Bezug auf eindeutige Kennzeichnungen:

$$ ((x, y), {x → 0, y → 0 }) ((y, x), {x → 0, y → 0 }) $$

Und das Gleiche gilt für $(1,1)$.Dies geht aus der Studie von hervor Spezies, wo man statt direkter Konstruktionen auf Typen in erster Linie daran denkt, verschiedene Formen beschrifteter Bäume zu kombinieren und die Beschriftungen dann den Werten zuzuordnen, die an der beschrifteten Position auftreten sollen.Die Diskrepanz entsteht dadurch, dass wir bei Arten normalerweise Strukturen berücksichtigen, an denen sich jede Position befindet deutlich beschriftet, wie $(0,1)$, während es bei Typen zu degenerierten Beschriftungen kommen kann, die keine Permutation erfordern, um Redundanzen zu beseitigen.

Es stimmt immer noch, dass z.B.Die Antwort von Conor McBride ist mit der Antwort von András verlinkt. Die Art der ungeordneten Paare ist ungefähr so $2^2/S_2$ als eine Art typtheoretischer Quotient durch Permutationen.Nur ist ein Teil der Quotientenbildung redundant, sodass Sie keine direkte Ganzzahlarithmetik durchführen können, um die Anzahl der resultierenden Werte zu zählen.Ein weiteres Beispiel hierfür wäre die Antwort: $$ℕ = e$$ durch Einstecken $\mathbf 1$ für $x$ in der Potenzreihe.Jedoch, alle die Permutationen sind in diesem Fall überflüssig.(Es gibt jedoch eine andere Vorstellung, wo dies funktioniert, Hier.)

Es ist möglich, eine Formel auszuarbeiten, mit der die Werte ungeordneter Paare endlicher Typen gezählt werden können.Ich denke, der einfachste Weg, dies zu tun, besteht darin, in Gesamtordnungen der endlichen Typen und geordneten Tupeln zu denken, die auch geordnete Komponenten haben müssen.Also $(0,0), (0,1), (1,1)$.Sie können vertreten $n$-Tupel endlicher Typen mit Größe $k$ indem $n$ Punkte mit $k-1$ Markierungen dazwischen, wobei die Markierungen angeben, wann Sie zu aufeinanderfolgenden Werten wechseln sollten.Die obigen Paare sind also: $$\cdot\cdot|\\ \cdot|\cdot\\ |\cdot\cdot$$ Ich habe die Formel dafür vergessen, aber es ist so etwas wie $n+k-1 \wähle n$ o.ä.