型境界

型境界は型指定に条件を加えるものである。これを実現する機能がガード(ガード節)である。 関数シグニチャ、無名関数シグニチャのほか、篩型でもこの機能を利用できる。 ガードは戻り値型の後に記述する。

述語式

変数の満たす条件を、Boolを返す式(述語式)で指定できる。 使用できるのは値オブジェクトと演算子だけである。コンパイル時関数は今後のバージョンで対応される可能性がある。

f a: [T; N] | T, N, N > 5 = ...
g a: [T; N | N > 5] | T, N = ...
Odd = {I: Int | I % 2 == 1}
R2Plus = {(L, R) | L, R: Ratio; L > 0 and R > 0}
GeneralizedOdd = {I | U; I <: Div(Nat, U); I % 2 == 0}