篩型

badge

Refinement type(篩型、ふるいがた)は、述語式によって制約付けられた型です。列挙型や区間型は篩型の一種です。

篩型の標準形は{Elem: Type | (Pred)*}です。これは、述語式Predを満たすElemを要素とする型である、という意味です。 Typeに使えるのはValue型のみです。

Nat = 0.._
Odd = {N: Int | N % 2 == 1}
Char = StrWithLen 1
# StrWithLen 1 == {_: StrWithLen N | N == 1}
[Int; 3] == {_: Array Int, N | N == 3}
Array3OrMore == {A: Array _, N | N >= 3}

複数のPredがあるとき、;かand, orで区切れます。;とandは同じ意味です。

Oddの要素は1, 3, 5, 7, 9, ...です。 篩にかけるように既存の型の一部を要素とする型になることから篩型と呼ばれます。

Predは(左辺)述語式と呼ばれます。これは代入式と同じく意味のある値を返すものではなく、左辺にはパターンしか置けません。 すなわち、X**2 - 5X + 6 == 0のような式は篩型の述語式としては使えません。この点において、右辺式の述語式とは異なります。

{X: Int | X**2 - 5X + 6 == 0} # SyntaxError: the predicate form is invalid. Only names can be on the left-hand side

あなたが二次方程式の解法を知っているならば、上の篩型は{2, 3}と同等になるだろうと予想できるはずです。 しかしErgコンパイラは代数学の知識をほとんど持ち合わせていないので、右の述語式を解決できないのです。

篩型の部分型付け規則

全ての篩型は、Type部で指定された型の部分型です。

{I: Int | I <= 0} <: Int

その他、現在のErgは整数の比較に関する部分型規則を持っています。

{I: Int | I <= 5} <: {I: Int | I <= 0}

スマートキャスト

Oddを定義したのはいいですが、このままではリテラル以外ではあまり使えないようにみえます。通常のIntオブジェクトの中の奇数をOddに昇格させる、つまりIntをOddにダウンキャストするためには、Oddのコンストラクタを通す必要があります。 篩型の場合、通常のコンストラクタ.newはパニックする可能性があり、.try_newというResult型を返す補助的なコンストラクタもあります。

i = Odd.new (0..10).sample!() # i: Odd (or Panic)

また、match中で型指定として使用することもできます。

# i: 0..10
i = (0..10).sample!()
match i:
    o: Odd ->
        log "i: Odd"
    n: Nat -> # 0..10 < Nat
        log "i: Nat"

ただし、Ergは現在のところOddでなかったからEven、などといった副次的な判断はできません。

列挙型、区間型と篩型

今まで紹介した列挙型と区間型は、篩型の糖衣構文です。 {a, b, ...}は{I: Typeof(a) | I == a or I == b or ... }に、a..bは{I: Typeof(a) | I >= a and I <= b}に脱糖されます。

{1, 2} == {I: Int | I == 1 or I == 2}
1..10 == {I: Int | I >= 1 and I <= 10}
1..<10 == {I: Int | I >= 1 and I < 10} == {I: Int | I >= 1 and I <= 9}

篩パターン

_: {X}をXと書き換えられるように(定数パターン)、_: {X: T | Pred}はX: T | Predと書き換えることができます。

# メソッド.mは長さ3以上の配列に定義される
Array(T, N | N >= 3)
    .m(ref self) = ...