量化依存型

Ergには量化型、依存型が存在します。すると当然、その二つを組み合わせた型を作ることができます。それが量化依存型です。

NonNullStr = |N: Nat| StrWithLen N | N != 0 # N: Nat; S: StrWithLen N; N != 0}と同じ
NonEmptyArray = |N: Nat| [_; N | N > 0] # N: Nat; A: Array(_, N); N > 0}と同じ

量化依存型の標準形はK(A, ... | Pred)です。Kは型構築子、A, Bは型引数、Predは条件式です。

左辺値としての量化依存型は、元の型と同じモジュール内でのみメソッドを定義出来ます。

K A: Nat = Class ...
K(A).
    ...
K(A | A >= 1).
    method ref! self(A ~> A+1) = ...

右辺値としての量化依存型は、使用する型変数を型変数リスト(||)で宣言する必要がある。

# Tは具体的な型
a: |N: Nat| [T; N | N > 1]