Lean
依存型 を搭載して定理証明の能力をもったプログラミング言語 匿名関数は fun x => x + 3 みたいなかんじ
-> を => にしたOCamlっすねえ 驚きはない
fun x => x + 3 には Nat -> Nat 型がつく
普通ですね
implicit arguments
Leanでは型も値として扱える
他言語でいうジェネリック引数も普通の引数になる
some (t) (v : t): Option t
ジェネリック引数はわりと省略が行われる
some<bool>(true) とか書かない、some(true) で十分
普通の言語で普通の引数は省略できない
つまり some Nat 3 みたいなのを毎回書かないといけなくなり、ダル
Leanでは some _ 3 とすることでimplicit argumentになり、いい感じに推論できたら推論される
関数の定義段階で some {t} (v : t): Option t としておくと some 3 でいい感じに推論してくれる
@some Nat 3 とすることで明示的に埋められる
some (3 : Int) とかもあるぞ