面向依赖类型语言的直接按需求值器
编程语言
2015-09-24 v1
摘要
我们通过扩展 Ariola、Chang 和 Felleisen 的（按需求值(call-by-need)）栈机以持有类型，采用无类型-无标签-最终(typeless-tagless-final)解释器策略，给出了 lambda-pi 演算的 C 语言实现。其优势在于将全部操作表达为对项的折叠，包括按需求值、任意项的初始语法树编码的恢复，以及消除大部分垃圾回收任务。这些得益于处理每项脊柱(spine)的规范化方法，以及健壮的基于栈的 API。类型推断不在本工作涵盖范围内，但也从当前的栈变换中获得若干优势。给出了执行基准问题的时间与最大栈空间使用结果。我们讨论了该解释器的设计选择如何使该语言可用作高级脚本语言，以对常见科学计算工作流进行自动分布式并行执行。
引用
@article{arxiv.1509.07036,
title = {Towards a Direct, By-Need Evaluator for Dependently Typed Languages},
author = {David M. Rogers},
journal= {arXiv preprint arXiv:1509.07036},
year = {2015}
}
备注
Submitted Version, 8 pages, 5 figures