Types for units-of-measure in f#: invited talk
Types for units-of-measure in f#: invited talk
复制标题
f 中的测量单位类型
DOI：
10.1145/1411304.1411305
复制
发表时间：
2008
期刊：
影响因子：
11.4
通讯作者：
A. Kennedy
中科院分区：
文献类型：
--
作者：
A. Kennedy
由量化单位错误造成的虫子可能会带来灾难性后果，其中最著名的是1999年9月在NASA的火星气候轨道探针中造成的损失，这是由纽顿（SI Of Force）与LBF之间的混乱引起的力单位）。
本演讲将描述F＃编程语言中静态检查和推断量级单位的支持。从程序员的角度来看，该功能并没有侵入性。数字常数带有其单位注释，用户定义的类型可以在单位上进行参数化，并且编译器将其剩下的，流动单位的信息进行到推断类型。在幕后，有许多技术微妙之处。类型推理算法通过使用（a）Abelian组统一来实现主类型，以及（b）在推断出乘数变量的多态性类型时进行的基本变化程序。类型方案以一致的样式呈现给程序员，该样式与线性代数的HERMITE正常形式有关。此外，还有许多有趣的交互作用，即F＃对面向对象的编程的支持。
当然，演讲将包括演示，还包括在机器学习，游戏编程，物理模拟和金融领域的案例研究。
Bugs caused by units-of-measure errors can have catastrophic consequences, the most famous of which was the loss in September 1999 of NASA's Mars Climate Orbiter probe, caused by a confusion between newtons (the SI unit of force) and lbf (the Imperial unit of force).
This talk will describe support for static checking and inference of units-of-measure in the F# programming language. From the programmer's perspective, the feature is not intrusive. Numeric constants are annotated with their units, user-defined types may be parameterized on units, and the compiler does the rest, flowing unit-of-measure information through to inferred types. Behind the scenes, there are a number of technical subtleties. The type inference algorithm achieves principal types through the use of (a) Abelian group unification and (b) a change-of-basis procedure when inferring polymorphic types for let-bound variables. Type schemes are presented to the programmer in a consistent style that is related to the Hermite normal form from linear algebra. In addition, there are a number of interesting interactions with F#'s support for object-oriented programming.
The talk will of course include a demonstration, and also a selection of case studies in the domains of machine learning, games programming, physics simulation, and finance.