モジュール

{ } でモジュールを定義できます。モジュール内の宣言はドット記法でアクセスします。

基本

cat = {
    u: *
    x: u → u
    m: x x → x
}

// モジュールのメンバーにアクセス
f: cat.u → cat.u

ネスト

モジュールはネストできます。

a = {
    b = {
        u: *
        x: u → u
    }
    y: b.u → b.u
}

// a.b.x でアクセス
f: a.b.x a.b.x → a.b.x

with 節

with { } で追加の宣言ができます。with 節の中では元の宣言のメンバーが直接使えます。

モジュールに使う場合:

cat = {
    u: *
    x: u → u
} with {
    m: x x → x
}

// cat.m も定義される

宣言に使う場合:

C: *
x: C → C with {
    m: x x → x
}

// x.m でアクセスできる

where 節

where { } でローカルな補助定義を書けます。where 節はモジュールだけでなく、一般の定義にも使えます。where 節の中の宣言は外部からはアクセスできません。

r[C: *, x: C → C, f: x → x]: x → x = g where {
    g = f; f
}

モジュールと組み合わせることもできます:

cat = {
    u: *
    x: u → u
    m: x x → x
} where {
    helper = x x; m
}

where 節はネストできます:

r[C: *, x: C → C, f: x → x]: x → x = k where {
    k = g; g
} where {
    g = f; f
}

内側の where 節が先に評価されます。上の例では g が先に定義され、それを使って k が定義されます。

+= によるメンバー追加

既存のモジュールや宣言にメンバーを追加できます。

f32: C → C

f32 += {
    lit[n: rat]: C → f32
    add: f32 f32 → f32
    neg: f32 → f32
}

// f32.lit[1], f32.add 等が使える

+= の右辺は { } モジュールです。追加されたメンバーは元の名前のドット記法でアクセスできます。これは sys ライブラリの内部で、型に演算を追加するために使われています。