Ich fange gerade an, Haskell zu lernen, nachdem ich aus den JavaScript / Ruby-Welten gekommen bin. Ich bin auf https://github.com/HoTT und das Buch Homotopy Type Theory gestoßen , das ich sehr gerne lese.
Im Laufe der Zeit werde ich jedoch die Konzepte der Mathematik und der Typentheorie lernen. Es scheint also lange zu dauern, bis ich verstehe, was die Homotopietypentheorie für einen praktizierenden Programmierer bedeutet.
Können Sie beschreiben, welchen Einfluss die Homotopietypentheorie auf die Programmierung in der Praxis für einen Laien haben wird? Wird es zum Beispiel bestimmte Dinge einfacher zu schreiben machen? Wenn ja, welche Dinge? Oder können Sie damit neue Dinge in der Programmierung tun, die vorher nicht möglich waren? Wenn ja, welche Dinge?
Vielen Dank, ich freue mich sehr darauf, meinen Kopf auf einer grundlegenderen Ebene darum zu wickeln.
quelle
Antworten:
Eines der mächtigsten Dinge, die Compiler während ihrer Optimierungsphase tun können, ist das Austauschen ineffizienter Darstellungen gegen gleichwertige. In Haskell können Sie beispielsweise eine Lazy-Liste verwenden, um eine Summe von Zahlen zu berechnen. Der GHC-Haskell-Compiler erkennt jedoch, dass dies der Verwendung einer Iteration mit einer temporären Variablen entspricht. Auf diese Weise können Sie gegen eine einfache Abstraktion programmieren, über die Sie leicht nachdenken können, während Ihre ausführbare Datei eine Darstellung nutzt, die besser für die Hardwareplattform geeignet ist (und die im Maßstab viel schwieriger zu überlegen ist).
Dem Compiler bekannte Äquivalenzen beschränken sich jedoch meist auf bekannte und erforschte Datenstrukturen, wie z. B. die Stream-Fusion für Listen. Sie könnten Ihre eigenen Äquivalenzen im Quellcode definieren (mithilfe eines Paares von Konvertierungsfunktionen, die sich in beide Richtungen zur Identität zusammensetzen), aber Sie müssten sie manuell anwenden, und es kann schwierig werden, den richtigen Typ für die Verwendung an allen Stellen auszuwählen um übermäßige Conversions zu vermeiden.
Stellen wir uns nun eine Welt vor, in der Sie "höherinduktive Typen" definieren können, beispielsweise eine kanonische Nachschlagekarte. Dieser Typ verfügt über mehrere Konstruktoren für die verschiedenen Arten von Karten: Binärsuche, AVL, Rot-Schwarz, Trie, Patricia usw. Neben den typischen Datenkonstruktoren definieren Sie auch einen Äquivalenztyp, der möglicherweise mehrere Konvertierungen zwischen diesen Darstellungen erfasst, sofern diese unterschiedlich sind Konvertierungen bieten unterschiedliche Effizienzdimensionen (dh Zeit vs. Speicher).
Was wäre, wenn der Compiler diesen Begriff verwenden könnte, um Kartendarstellungen transparent neu zu schreiben, so wie es heute bei der Listenfusion der Fall ist? Währenddessen können Sie in Ihrem Code mit der Konstruktion arbeiten, die am einfachsten zu begründen ist (und die Beweisarbeit erleichtert, wenn Sie sich in einer solchen Umgebung befinden). Dies mag sich wie eine abstrakte Schnittstelle mit mehreren Implementierungen anhören, beinhaltet jedoch die Freiheit, eine beliebige Implementierung auszuwählen und den Compiler bei Bedarf transparent durch eine andere ersetzen zu lassen, ohne die Bedeutung des Programms zu beeinträchtigen.
HoTT gibt uns eine typentheoretische Grundlage, um diesen ausgefallenen Umschreibemechanismus und diese reich definierten Typen zu rechtfertigen, da es den Begriff der Äquivalenz fördert, gleichbedeutend mit Gleichheit zu sein. Es bleibt abzuwarten, wie sich dies in der Praxis tatsächlich auswirken wird, aber es gibt uns den theoretischen Rahmen, auf dem zukünftige Arbeiten basieren können.
quelle