第22章 ニュータイプと篩型

この章の目的

この章の終わりまでに、型に独自の名前を与え、そのすべての値が満たさなければならない規則を付与できるようになります。

見た目が似た数の問題

チャンネル番号は Word です。ノートのベロシティは Word です。MIDI ピッチは Word です。これらはすべて整数であり、そのため言語は、そのままにしておくと、そのうちのどれかを別のものが意図された場所で使わせてしまいます。チャンネルを期待する関数にベロシティを渡すことは実際の誤りであり、3つすべてが同じ型であるため、Word 型が捕捉できない誤りです。

ニュータイプ、すなわち独自の名前

ニュータイプは、基礎となる型に新しい独自の名前を与えます。

newtype Channel = Word;

fn raw(c: Channel) -> Word {
    c as Word
}

fn main() -> Word {
    raw(Channel(2))
}

keleusma run で実行してください。出力は 2 です。

内部的には、Channel は Word であり、まったく同じ速さで動作します。しかし型システムにとっては、Channel と Word は異なる型です。Channel は Channel(2) と書くことで構築されます。基礎となる Word は c as Word と書くことで取り戻されます。言語は、それらの明示的な手順のいずれかなしに、Channel が期待される場所で素の Word を使うこと、あるいはその逆を許しません。見た目が似た数は、これで別々に保たれます。

篩、すなわち規則を伴う名前

ニュータイプは、篩と呼ばれる規則を持つことができます。その規則は、基礎となる値を取り true または false を答える通常の関数です。

fn in_range(x: Word) -> bool {
    x >= 0 and x <= 127
}

newtype Velocity = Word where in_range;

fn raw(v: Velocity) -> Word {
    v as Word
}

fn main() -> Word {
    let soft = Velocity(40);
    raw(soft)
}

実行してください。出力は 40 です。MIDI ベロシティは 0 から 127 の間になければなりません。where in_range 節はその規則を Velocity に付与します。Velocity が構築されるたびに、その規則が検査されます。値 40 は通過するので、Velocity(40) は成功します。

壊れた値は捕捉されます

範囲外のベロシティを構築するようにプログラムを変更してください。

fn main() -> Word {
    raw(Velocity(200))
}

実行すると、結果はなく、次のものだけが得られます。

error: compile: refinement check `in_range` provably fails for newtype `Velocity` at compile time on argument 200

値 200 はプログラムに書き込まれているため、言語はその場でその規則を検査し、プログラムが実行される前に、それを拒否します。Velocity は単に範囲外の数を保持できません。where 節に一度書かれたその規則は、すべての構築で強制されます。それは、誤った音符が演奏されえないように書かれたパートです。

この章のまとめ

• newtype Name = Underlying; は、基礎となる型に独自の名前を与えます。
• Name(value) は1つを構築します。value as Underlying は基礎となる値を取り戻します。
• newtype Name = Underlying where predicate; は規則を付与し、すべての構築で検査されます。
• 規則を証明可能に破る構築は、プログラムが実行される前に拒否されます。
• 値が実行時にのみ規則を破りうる場合、ニュータイプ構築の構文 Name(value) { ok(v) => ..., invalid_newtype(x) => ... } がその場で拒否を処理します。第23章を参照してください。

次の章では、上記の構築の拒否を含め、失敗しうる操作を扱います。