Space-efficient gradual typing
Space-efficient gradual typing
复制标题
节省空间的渐进打字
DOI：
10.1007/s10990-011-9066-z
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
C. Flanagan
中科院分区：
文献类型：
--
作者：
David Herman;Aaron Tomb;C. Flanagan
渐进类型系统通过允许类型化和非类型化代码的自由混合，在静态和动态类型化之间提供了一个平滑的连续体。这些语言和其他具有混合类型检查的语言的运行时系统通常通过动态生成函数代理来强制执行函数类型。这种方法可能会导致无限增长的代理的数量，但是，这极大地影响了空间效率和破坏尾recursion.We提出了一个语义逐步类型，是基于代理而不是函数代理，并结合相邻的代理在运行时，以限制其空间消耗。我们证明了边界上消耗的空间的类型系统的可靠性，以及，程序员可以安全地混合打字纪律，而不会产生不合理的开销。我们的方法也比以前的工作更早地检测到某些错误。
Gradual type systems offer a smooth continuum between static and dynamic typing by permitting the free mixture of typed and untyped code. The runtime systems for these languages, and other languages with hybrid type checking, typically enforce function types by dynamically generating function proxies. This approach can result in unbounded growth in the number of proxies, however, which drastically impacts space efficiency and destroys tail recursion.We present a semantics for gradual typing that is based on coercions instead of function proxies, and which combines adjacent coercions at runtime to limit their space consumption. We prove bounds on the space consumed by coercions as well as soundness of the type system, demonstrating that programmers can safely mix typing disciplines without incurring unreasonable overheads. Our approach also detects certain errors earlier than prior work.