Dimension Types
Dimension Types
复制标题
尺寸类型
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
A. Kennedy
中科院分区：
文献类型：
--
作者：
A. Kennedy
科学家和工程师必须确保物理方程在量纲上是一致的，但现有的编程语言将所有数值都视为无量纲的。本文在强类型程序设计语言中引入了维类型的概念。我们的方法改进了以前的建议，维度类型可能是多态的。此外，任何表达式，这是在系统中的类型有一个最一般的类型，我们描述了一个算法，自动推断这种类型。该算法利用方程的阿贝尔群的统一，除了普通的长期统一。描述了类型系统的实现，扩展了ML Kit编译器。最后，我们讨论的问题，获得一个标准形式的主要类型和素描一些更强大的系统，使用依赖和高阶多态类型。
Scientists and engineers must ensure that physical equations are dimensionally consistent, but existing programming languages treat all numeric values as dimensionless. This paper extends a strongly-typed programming language with a notion of dimension type. Our approach improves on previous proposals in that dimension types may be polymorphic. Furthermore, any expression which is typable in the system has a most general type, and we describe an algorithm which infers this type automatically. The algorithm exploits equational unification over Abelian groups in addition to ordinary term unification. An implementation of the type system is described, extending the ML Kit compiler. Finally, we discuss the problem of obtaining a canonical form for principal types and sketch some more powerful systems which use dependent and higher-order polymorphic types.