物理次元型を持つ静的型付け言語「Numbat」の紹介 #Rust – Qiita

「マーズ・クライメイト・オービター」をご存知でしょうか。火星の気象調査をミッションとして、NASAが1998年に打ち上げた探査機です。1億2500万ドルを費やして作られたこの探査機は、本務に就く前に火星周回軌道内で炎上、そのまま消息を絶ちました。原因はヤード・ポンド法単位とメートル法単位の取り違え。

かの有名な「もう助からないゾ♡」の事故もやはり単位変換ミスが発端でした。人類史上において、不適切な単位の取り扱いが悲惨な事故に繋がる例は枚挙にいとまがありません。

プログラミングにおいても同じです。接頭辞の変換を忘れたり、numpyの三角関数にradianではなくdegreeで角度を与えて時間を溶かした人は私だけではないでしょう¹。もっと安全・便利に数値を扱えるように人類をサポートする仕組みが必要です。

……そんな感じの問題意識から生まれたプログラミング言語、それが「Numbat」です。

Numbatは、科学技術計算を安全かつ効率的に行うことを目的する静的型付け言語です。この言語は、物理次元（長さ、時間、質量など）をファーストクラスの型として扱うことで、単位の不適切な取扱いを型エラーとして検出できます。単位変換はすべて自動で行われ、書き手が自分で行う必要はありません。

まず特徴的なのが代入操作です。数値型の場合、let [変数名]: [型名] = [数値] [単位]の形で変数に値を代入します。型名はLength, Time, Mass等の物理次元の名前になります（無次元量はScalar）。

let w1: Mass = 0.5 kg
# let [変数名]: [型名（物理次元）] = [数値] [単位]

ただし、型推論が働くので、型名は省略しても構いません。

let w2 = 2 lb
# w2に2ポンドを代入

変数同士は、単位変換を行うことなく演算が可能です。printで出力する際、-> [単位]とすることで、出力単位を指定できます。

print(w1 + w2 -> oz)
# -> 49.637 oz | オンスとしてprint

つまり、値を与える時と値を取り出す時にさえ単位を指定すれば、その間の変換について一切考えることなく演算結果を得ることが出来ます。

オンラインPlaygroundで、インタラクティブにNumbatの挙動を試すことが出来ます。
以下に公式のサンプルを示します。

Numbatの関数は引数や返値に次元型が指定されているため、次元が合っていれば、どのような単位で値を入力しても正しい答えを返すことができます。例えば、下記のように余弦関数cos()に対してradianで指定した角度（π/3）を入れても、degreeで指定した角度（60°）を入れても、正しい答え（0.5）が得られます。どちらもAngleの次元を持つためです。

let ω: Angle = π/3 rad
# 角度をラジアンで指定

let δ: Angle = 60°
# 角度を度数で指定

print(cos(ω))
# -> 0.5

print(cos(δ))
# -> 0.5

print(cos(ω + δ))
# -> -0.5

逆に、次元が合っていなければ、きちんとエラーが返ってきます。例えば、下記のように余弦関数cos()に対してLengthの次元を持つαを引数として与えると、

let α = 3 nm
print(cos(α))

エラーが発生し、「次元が合っていませんよ」と教えてくれます。そのまま演算を実行して無意味な答えを返すことはありません。

error: while type checking
  ┌─ Module 'math::trigonometry', File /usr/share/numbat/modules/math/trigonometry.nbt:9:8
  │
9 │ fn cos(x: Scalar) -> Scalar
  │        ^ Angle or Scalar or SolidAngle
  │
  ┌─ File calc.nbt:2:11
  │
2 │ print(cos(α))
  │       --- ^ Length
  │       │    
  │       incompatible dimensions in argument 1 of function call to 'cos'
  │
  = parameter type: Scalar    [= Angle, Scalar, SolidAngle]
     argument type: Length
    
    Suggested fix: divide the function argument by a `Length` factor

Interpreter stopped

異なる次元を持つ数値同士の加算・減算も当然認められていません。

let memory_size = 2 MB
let cache_size = 1_048_576 bit

print(memory_size + cache_size -> kB)
# -> 2131.07 kB | 単位は異なるが次元は同じ（DigitalInformation） なので加算OK

let heart_rate = 90 bpm
print(memory_size + heart_rate)
# エラー: DigitalInformation + Frame/Time は次元が異なるので出来ない

このように、数値に対して常に次元型を用いたチェックを行うことで、柔軟かつ安全な計算プログラムを書くことが可能になります。

物理単位の換算を自動で行ってくれるようなライブラリ自体は多数存在します。PythonのPintとか、JuliaのUnitful.jlあたりが有名でしょうか。言語標準の型システム内で物理単位を扱えるという点では、F#のUnits of Measureも近いコンセプトです²。これらと比較した際のNumbatの特徴は以下の通りです。

1. 言語全体が静的な物理次元型を前提としている

let Eₚ: Energy = 80 kg × 9.8 m/s² × 5 m

fn max_distance(v: Velocity, θ: Angle) -> Length = v² · sin(2 θ) / g0

fn sqrtD>(x: D^2) -> D
# 平方根関数。引数は返り値の2乗の次元を持つ

fn sqrtD>(x: D) -> D^(1/2)
# 同上

print(π)
# -> 3.14159
print(pi)
# -> 3.14159
print(avogadro_constant)
# -> 6.02214e+23 mol⁻¹

let msg: String = "Hello, World!"
print(msg)
# -> Hello, World!

[1 m, 1e4 mm, NaN, -inf] 
                |> filter(is_finite) 
                |> sum()
                
# -> 11 m    [Length]
# リストの中から有限の値を持つ（is_finite）要素のみfilterし、それらの合計をsumで取得

fn step(x) = if x  0 then 0 else 1
# xが0以上の時に1、そうでない時に0を与えるステップ関数

unit TokyoDome: Volume = 1_240_000 m³
# Volume次元を持つ新単位「東京ドーム」を定義

>>> print(planck_leng)
error: while type checking
  ┌─ ││││35>