-
Notifications
You must be signed in to change notification settings - Fork 4
Release 0.4.0
らいパン粉 edited this page Oct 20, 2018
·
14 revisions
infixl 0 +;
id::(Fn Int32->Int32)->(Fn Int32->Int32);
id x = x;
main = (id (\x->x+2)) 5;
infixl 0 +;
add::Int32->Fn[Int32]Int32->Int32;
add x = \[x]y->x+y;
main = (add 4) 5;
infixl 0 +;
main = (\x,y,z->x+y+z)x y z;
//構文------------------------
//top level
tt :=
t
tt op tt
//演算子
op := +
-
/
*
//項
t :=
n //数値
x //変数
λx.t //ラムダ抽象
t t //関数適応
(tt)
//値
v := n
x
λx.t
//文脈
ctx := φ //空文脈
ctx ∪ x:T //変数の束縛
//評価---------------------------
//演算子適応
tt1 op tt2 => tt1 op tt2' (tt2=>tt2')
tt1 op v2 => tt1' op v2 (tt1=>tt1')
v1 op v2 => v3
//関数適応
t1 t2 => t1' t2 (t1 => t1')
(λx.t12) t2 =>[x->t2]t12
//括弧
(tt1)=>(tt1') (tt1=>tt1')
(v1) =>v1
//型
T := i32
T->T
//型つけ---------------------------
//変数
x:T (x:T ∈ ctx)
//関数適応
t1 t2 :T12 (t1:T11->T12 かつ t2:T11)
//数値
n:i32
//演算子
tt1 op tt2 :i32 (tt1:i32 , tt2:i32)
//括弧
(tt1) :T (tt1 :T)