计量单位类型：理论与实践

# 计量单位类型：理论与实践 ## 1. 引言 计量单位之于科学，就如同类型之于编程。在科学和工程领域，维度和单位的一致性为方程或公式的正确性提供了初步检查，就像在编程中，类型检查器对程序的验证消除了一种可能的失败原因。 计量单位错误可能会造成灾难性后果，其中最著名的是 1999 年 9 月美国国家航空航天局（NASA）的火星气候轨道器探测器的损失，这是由于牛顿（国际单位制中的力单位）和磅力（美国有时使用的力单位）之间的混淆导致的。多年来，许多人提出了扩展编程语言以支持计量单位静态检查的方法。本文将介绍 F# 编程语言对计量单位的支持、其类型系统的内部机制以及单位安全的理论基础。 ### 1.1 教程内容 本教程分为三个部分： 1. **F# 中计量单位的编程指南**：面向有函数式编程背景的程序员。 2. **类型系统和推理算法的详细信息**。 3. **单位语义的探讨**：包括与经典维度分析的联系。 教程最后会有简短的讨论，每个部分都包含一些练习，部分练习的解决方案可在附录中找到。 ## 2. F# 中计量单位的介绍 要使用 F# 的计量单位功能，你需要 F# 命令行编译器（fsc）和交互式环境（fsi），也可以选择使用 Visual Studio 集成开发环境（仅适用于 Windows）。 ### 2.1 引入单位 首先，我们要声明一些基本单位。在 21 世纪，我们采用国际单位制（SI），声明质量、长度和时间的单位： ```fsharp [<Measure>] type kg // kilograms [<Measure>] type m // metres [<Measure>] type s // seconds ``` `<Measure>` 属性表明我们引入的不是常规意义上的类型，而是计量单位构造函数，即 `kg`、`m` 和 `s`。 接下来，我们可以为一个著名的常量添加单位，只需将单位添加到浮点字面量的尖括号中： ```fsharp let gravityOnEarth = 9.808<m/s^2> // an acceleration ``` 这里使用了常规的单位表示法，`/` 表示除法，`^` 表示幂运算。我们也可以用不同的方式表示加速度的单位： ```fsharp let gravityOnEarth = 9.808<m * s^-2> let gravityOnEarth = 9.808<m/s/s> ``` 在 F# 交互式环境中，编译器会告诉我们 `gravityOnEarth` 的类型： ```fsharp > let gravityOnEarth = 9.808<m/s/s>;; val gravityOnEarth : float<m/s ^ 2> = 9.808 ``` `float` 类型可以用计量单位进行参数化，就像 `list` 可以用类型参数化一样。 现在我们可以进行一些物理计算。如果一个物体从 40 米高的建筑物上掉落，它落地时的速度是多少呢？根据牛顿动力学公式 $\sqrt{2gh}$（其中 $g$ 是重力加速度，$h$ 是高度），我们可以在 F# 中进行计算： ```fsharp > let heightOfBuilding = 40.0<m>;; val heightOfBuilding : float<m> = 40.0 > let speedOfImpact = sqrt (2.0*gravityOnEarth*heightOfBuilding);; val speedOfImpact : float<m/s> = 28.01142624 ``` 可以看到，计量单位会自动计算。当我们进行乘法、除法或平方根运算时，单位也会相应地进行运算。 如果我们犯了错误，比如尝试将高度和加速度相加： ```fsharp > let speedOfImpact = sqrt (2.0*gravityOnEarth+heightOfBuilding);; let speedOfImpact = sqrt (2.0*gravityOnEarth+heightOfBuilding);; ---------------------------------------------^^^^^^^^^^^^^^^^ stdin(142,50): error FS0001: The unit of measure ’m’ does not match the unit of measure ’m/s ^ 2’ ``` F# 会准确地告诉我们错误所在。在 Visual Studio 中，错误会以红色波浪线显示，鼠标悬停时会显示错误信息。 我们再进行一个物理计算，根据牛顿第二定律，地面为了维持我的静止位置对我施加的力是多少呢？ ```fsharp > let myMass = 65.0<kg>;; val myMass : float<kg> = 65.0 > let forceOnGround = myMass*gravityOnEarth;; val forceOnGround : float<kg m/s ^ 2> = 637.52 ``` 牛顿的同名单位“牛顿”是力的国际单位制单位。我们可以引入一个派生单位 `N` 来简化表示： ```fsharp [<Measure>] type N = kg m/s^2 let forceOnGround:float<N> = myMass*gravityOnEarth ``` 派生单位就像类型别名，在类型检查方面，`N` 和 `kg m/s^2` 是等价的。但 F# 在显示类型时不会自动识别派生单位。 ### 2.2 F# PowerPack 的使用 F# 的 “PowerPack” 库声明了所有的 SI 基本单位和派生单位，位于 `Microsoft.FSharp.Math.SI` 命名空间，还在 `Microsoft.FSharp.Math.PhysicalConstants` 命名空间中定义了各种物理常量。 要导入这个库，在 Visual Studio 中，你可以右键点击 “References”，选择 “FSharp.PowerPack” 组件；或者在 fsi 中使用 `#r` 指令： ```fsharp > #r "FSharp.PowerPack";; --> Referenced ’C:\Program Files\FSharp\bin\FSharp.PowerPack.dll’ ``` 现在我们可以使用 PowerPack 中的单位和常量来实现牛顿万有引力定律： ```fsharp > open Microsoft.FSharp.Math;; > open SI;; > let attract (m1:float<kg>) (m2:float<kg>) (r:float<m>) : float<N> = - PhysicalConsta ```