Typen werden vor der Laufzeit gelöscht

Question

Ich weiß sicher, dass in Haskell Typen vor der Laufzeit immer gelöscht werden. Was passiert im Falle von Agda?

Wird abhängige Typinformation zur Laufzeit übertragen?

Answer 1

Welche Laufzeit? Es gibt mindestens vier Backends: diejenigen, die auf GHC (genannt MAlonzo), UHC, Epic und JavaScript abzielen. Einige erste Details finden Sie in : Sie können lesen, wie das Epic-Backend Typen dort oder in diesem paper löscht (das Kapitel "3.3 Erasure"). Kurz gesagt, die Epic- und UHC-Backends löschen alle Typen, die eine vollständig angewendete Funktion empfängt, führen jedoch kein vollständiges Löschen durch, da sie die Semantik eines Programms (paper über das UHC-Backend) ändern können:

Typ Übersetzung

Die übrigen Bedingungen Π, Set und Level sind signifikant für Typ nur zu prüfen. In Agda kann ein Wert des Typs Set oder Level nicht überprüft oder Muster angepasst werden. Da Agda diese erzwingt, ist es unmöglich, irgendeinen Wert dieser Typen zu beobachten, sie können die Laufzeit-Semantik nicht beeinflussen . Für die Ausführung eines Programms ist es daher sicher, alle Vorkommen solcher Werte durch den Einheitswert ⊤ zu ersetzen.

Man könnte auch versucht sein, alle Werte dieser Art vollständig zu entfernen. Dies könnte möglicherweise die Semantik des übersetzten Programms verändern. Agda wertet Ausdrücke unter Lambda nicht aus; Droping Lambda Abstraktionen nehmen Typ Ausdrücke könnte Auswertung-Blockierung Lambdas entfernen. Ein teilweises Löschen von Typen ist in ein solider Weg möglich. Gesättigte Funktionsanwendungen können zum Beispiel immer auf diese Weise optimiert werden. Eine genauere Beschreibung, wann solche Typen gut gelöscht werden können, findet sich in früheren Arbeiten von Letouzey.