値と型

Yulang の値と型、関数型、effect row、type variable、role constraint をまとめる。 推論結果に現れる union と intersection も扱う。

Primitive types

Type	例
int	0, 42, -7
float	3.14, -0.5
bool	true, false
str	"hello"
()	unit 値
never	返らない式の型

Tuple

(1, "hello", true)

tuple は位置で持つ product。 my (a, b, c) = triple のように pattern で分解できる。

List

[1, 2, 3]

'a の list は list 'a。 xs[i] は Index role を通して解決される。

Record

{ x: 3, y: 4 }
{ ..base, x: 3 }
{ x: 3, ..rest }

anonymous な named product である。 field access は .field。

record pattern は default によって field を省略可能にできる。

my width_or_default { width = 1 } = width
my keep_input { width, ..input } = input

型表示では、省略可能な record field は ? 付きで出る。 たとえば {width?: α} -> α | int のような形である。 spread binding は、明示的に名前を挙げた field も含む入力 record 全体を受け取る。 keep_input の generic な型は ('a & {width: 'b}) -> 'a | {width: 'b, ..never} である。

Optional

just 42
nil

opt 'a は標準ライブラリの enum opt 'a = nil | just 'a である。 prelude は型と variant の両方を reexport する。 通常のコードでは std::data::opt:: や opt:: を付けずに opt、just、nil と書く。

Result

ok 1
err "bad"

result 'ok 'err は fallible computation を値として返すための標準型である。 prelude は result、ok、err を reexport するため、local name と衝突する場合だけ修飾する。

Range

0..<10  // 0 から 9
0..10   // 0 から 10
0..     // 0 から無限

..、..<、<..、<..< は std::data::range の range operator である。 range は Fold を実装するため、for x in r: と nondeterminism の each collector で使える。

Type variable

type variable は 'a のように書き、型注釈の中へ直接出す。 普通の関数 binding では、type variable だけを先に宣言する引数リストはない。

my id(x: 'a): 'a = x

型推論は、多くの場合 type variable を自動で埋める。 注釈は型を明示する場合や、曖昧さを解消する場合に使う。

Value restriction

Yulang は、binding の右辺が構文上の値である場合だけ一般化する。 したがって、関数値には多相 scheme が付く。

my id = \x -> x

(id 1, id "text")

計算する右辺は、同じ表示形の関数を返す場合でも一般化しない。

my id = (\f -> f) (\x -> x)

id

後者の id は type variable を量化せず、1 個の monomorphic scheme に保持する。 subtyping によって異なる入力形の呼び出しが通る場合もあるため、呼び出しの成功だけでは computed binding の一般化を確認できない。

再帰関数の binding は、許可された strongly connected component（SCC）を作る。

my even n = if n == 0: true else: odd (n - 1)
my odd n = if n == 0: false else: even (n - 1)

(even 10, odd 9)

computed value の cycle は、一方の binding を評価するために他方の computation を取得するので拒否される。

my make x = x
my a = make b
my b = make a

a

この cycle に対して、checker は computed value fetch in recursive component を報告する。

as による inline ascription

binding ascription (my x: T = e) や引数 ascription (my f(x: T) = ...) は : を使うが、式の途中で部分式に型を当てたいときは as を使う。

([] as list int)
(nil as opt str)
my n = (read_input() as int) + 1

inline の : は colon application (f: x) に予約されているので、式位置の (e : T) を許すと衝突する。 多相値の型を my binding を立てずにその場で固定したいときは as を使う。

関数型と effectful computation

int -> int
() -> [console] str
[console] str

A -> B は関数型である。 返り値側で effect を起こす関数は、返り値側に effect row を持つ。

() -> [console] str

[console] str は console effect を起こし得る computation 値である。 返り値は str である。 handler や control abstraction の引数で使える。

our run_console(action: [console] 'a): 'a = catch action:
    console::read(), k -> run_console(k "42")

型表示では α [io; β] -> [β] α のように、関数の引数側にも effect row が出ることがある。 これは「引数が effectful computation である」という意味である。 source 注釈では、[io; 'e] 'a のように具体的な値型か type variable を置く。

_ は注釈内で推論に穴埋めを任せる placeholder として使える。 型 constructor ではなく、基礎となる型構文の一部でもない。

Effect row

[console; 'e] str
() -> [console; 'e] str

row は named effect の列と、任意の残りを表す row variable ; 'e を持てる。 [_] のような wildcard row は注釈 placeholder である。 effect row 型そのものの標準形ではない。

Role constraint

my twice(x: 'a) =
    where 'a: Add
    x.add x

where は type variable が role を実装していることを要求する。 同じ形式を binding body、role body、impl body で使える。

推論された union / intersection

Yulang の推論結果には、union や intersection が表示されることがある。 ただし、それらを source 注釈として直接書くための安定した構文はまだない。

α | int
α & {width?: ⊤}

分岐、default 値、pattern spread などで複数の形が残ると、Types pane にこのような型が出る。 注釈を足すと、表示型を意図した公開形へ絞れることが多い。

関連

• effect：effect の宣言、呼び出し、handler。
• 型推論の理論：subtyping、effect row、handler hygiene の内部的な見方。