类型在运行时间之前被删除

Question

我确信在Haskell类型中总是在运行时之前擦除.在Agda的情况下会发生什么？

是否将依赖类型信息传递给运行时？

Answer 1

什么运行时间？至少有四个后端：针对 GHC（称为 MAlonzo）、UHC、Epic 和 JavaScript 的后端。一些初始细节可以在Agda wiki中找到：您可以在那里或本文（“3.3 擦除”章节）中阅读 Epic 后端如何擦除类型。简而言之，Epic 和 UHC 后端会擦除完全应用的函数接收到的所有类型，但不会执行完全擦除，因为它可以更改程序的语义（引用自有关 UHC 后端的论文）：

\n\n

\n

类型翻译

\n\n

其余术语\xce\xa0、Set和Level\n 仅对于类型检查有意义。在 Agda 中，无法检查或模式匹配Setor\n 类型的值。Level由于 Agda 强制要求不可能观察到这些类型的任何值，因此它们不能影响运行时语义。因此，为了执行程序，用单位值替换所有出现的此类值是安全的\xe2\x8a\xa4。

\n\n

人们也可能会想要完全删除这些类型的任何值。这可能会改变翻译后的程序的语义。Agda 不计算 lambda 下的表达式；删除采用类型表达式的 lambda 抽象可能会删除阻塞计算的 lambda。可以通过合理的方式部分擦除类型。例如，饱和功能应用程序始终可以通过这种方式进行优化。关于何时可以彻底删除此类类型的更详细描述可以在 Letouzey 之前的工作中找到。

\n

\n