¤Þ¤º¡¤ML2 ¤Î¼°¤ËÂФ·¤Æ¤Î·¿¿äÏÀ¤ò¹Í¤¨¤ë¡¥ML2¤Ç¤Ï¡¤ ¥È¥Ã¥×¥ì¥Ù¥ëÆþÎϤȤ·¤Æ¡¤¼°¤À¤±¤Ç¤Ê¤¯letÀë¸À¤òƳÆþ¤·¤¿¤¬¡¤¤³¤³¤Ç¤Ï¤Ò¤È¤Þ¤º ¼°¤Ë¤Ä¤¤¤Æ¤Î·¿¿äÏÀ¤Î¤ß¤ò¹Í¤¨¡¤letÀë¸À¤Ë¤Ä¤¤¤Æ¤ÏºÇ¸å¤Ë°·¤¦¤³¤È¤Ë¤¹¤ë¡¥ ML2¤Îʸˡ¤Ï(µË¡¤Ï¿¾¯°Û¤Ê¤ë¤¬)°Ê²¼¤Î¤è¤¦¤Ç¤¢¤Ã¤¿¡¥
|
¤³¤³¤Ç¤Ï <¼°> ¤ÎÂå¤ï¤ê¤Ë e ¤È¤¤¤¦µ¹æ(¥á¥¿ÊÑ¿ô)¡¤<¼±ÊÌ»Ò> ¤ÎÂå¤ï¤ê¤Ë x ¤È¤¤¤¦µ¹æ(¥á¥¿ÊÑ¿ô)¤òÍѤ¤¤Æ¤¤¤ë¡¥ ¤Þ¤¿¡¤·¿(¥á¥¿ÊÑ¿ô τ)¤È¤·¤Æ¡¤À°¿ô¤òɽ¤¹ int, ¿¿µ¶Ãͤòɽ¤¹ bool¤ò¹Í¤¨¤ë¡¥
τ ::= int | bool |
¤µ¤Æ¡¤·¿¿äÏÀ¤Î¥¢¥ë¥´¥ê¥º¥à¤ò¹Í¤¨¤ëÁ°¤Ë¡¤¤½¤â¤½¤â¡Ö¼° e ¤¬·¿ τ ¤ò»ý¤Ä¡×¤È¤¤¤¦´Ø·¸¤¬¤É¤Î¤è¤¦¤Ê»þ¤ËÀ®Î©¤¹¤ë¤«¤òÀµ³Î¤Ëµ½Ò¤·¤¿¤¤¡¥ Î㤨¤Ð¡Ö¼° 1+1 ¤Ï·¿ int ¤ò»ý¤Ä¡×¤À¤í¤¦¤¬¡¤ ¡Ö¼° if 1 then 2+3 else 4 ¤Ï·¿ int ¤ò»ý¤Ä¡×¤Ï À®Î©¤·¤Ê¤¤¤È»×¤ï¤ì¤ë¡¥¤³¤Î¡¤¡Ö¼° e ¤¬·¿ τ ¤ò»ý¤Ä¡× ¤È¤¤¤¦È½ÃǤò·¿È½ÃÇ(type judgment)¤È¸Æ¤Ó¡¤e : τ ¤Èάµ¤¹¤ë¡¥
¤·¤«¤·¡¤°ìÈ̤˼°¤Ë¤ÏÊÑ¿ô¤¬¸½¤ì¤ë¤¿¤á¡¤Î㤨¤Ðñ¤Ë x ¤¬ int ¤ò»ý¤Ä¤«¡¤¤È¤¤¤ï¤ì¤Æ¤âȽÃǤ¹¤ë¤³¤È¤¬¤Ç¤¤Ê¤¤¡¥¤³¤Î¤¿¤á¡¤ÊÑ¿ô¤ËÂФ·¤Æ¤Ï¡¤¤½ ¤ì¤¬»ý¤Ä·¿¤ò²¿¤«²¾Äꤷ¤Ê¤¤¤È·¿È½ÃǤϲ¼¤»¤Ê¤¤¤³¤È¤Ë¤Ê¤ë¡¥¤³¤Î¡¤ÊÑ¿ô¤Ë ÂФ·¤Æ²¾Äꤹ¤ë·¿¤Ë´Ø¤¹¤ë¾ðÊó¤ò·¿´Ä¶(type environment)(¥á¥¿ÊÑ ¿ôΓ)¤È¸Æ¤Ó¡¤ÊÑ¿ô¤«¤é·¿¤Ø¤ÎÉôʬ´Ø¿ô¤Çɽ¤µ¤ì¤ë¡¥¤³¤ì¤ò»È¤¨¤Ð¡¤ ÊÑ¿ô¤ËÂФ¹¤ë·¿È½ÃǤϡ¤Î㤨¤Ð
Γ(x) = int ¤Î»þ x: int ¤Ç¤¢¤ë
¤È¸À¤¨¤ë¡¥¤³¤Î¤³¤È¤ò¹Íθ¤ËÆþ¤ì¤Æ¡¤·¿È½ÃǤϡ¤Γ⊢ e : τ ¤Èµ½Ò¤·¡¤
·¿´Ä¶ Γ ¤Î²¼¤Ç¼° e ¤Ï·¿ τ ¤ò»ý¤Ä
¤ÈÆɤࡥ⊢ ¤Ï¿ôÍýÏÀÍý³Ø¤Ê¤É¤Ç»È¤ï¤ì¤ëµ¹æ¤Ç¡Ö¡Á¤È¤¤¤¦²¾Äê¤Î²¼¤ÇȽ ÃÇ¡Á¤¬Æ³½Ð¡¦¾ÚÌÀ¤µ¤ì¤ë¡×¤¯¤é¤¤¤Î°ÕÌ£¤Ç¤¢¤ë¡¥¥¤¥ó¥¿¥×¥ê¥¿¤¬(ÊÑ¿ô¤ò´Þ¤à) ¼°¤ÎÃͤò·×»»¤¹¤ë¤¿¤á¤Ë´Ä¶¤ò»È¤Ã¤¿¤è¤¦¤Ë¡¤·¿¿äÏÀ´ï¤¬¼°¤Î·¿¤ò·×»»¤¹¤ë¤¿ ¤á¤Ë·¿´Ä¶¤ò»È¤Ã¤Æ¤¤¤ë¤È¤â¹Í¤¨¤é¤ì¤ë¡¥
·¿È½ÃǤϡ¤·¿ÉÕ¤±µ¬Â§(typing rule)¤ò»È¤Ã¤ÆƳ½Ð¤µ¤ì¤ë¡¥ ·¿ÉÕ¤±µ¬Â§¤Ï°ìÈÌ¤Ë [<µ¬Â§Ì¾>] <·¿È½ÃÇ1> ⋯<·¿È½ÃÇn> <·¿È½ÃÇ> ¤È¤¤¤¦·Á¤Ç½ñ¤«¤ì¡¤²£Àþ¤Î¾å¤Î<·¿È½ÃÇ1>,…, <·¿È½ÃÇn>¤òµ¬Â§¤ÎÁ°Äó(premise)¡¤ ²¼¤Ë¤¢¤ë<·¿È½ÃÇ>¤òµ¬Â§¤Î·ëÏÀ(conclusion)¤È¸Æ¤Ö¡¥ Î㤨¤Ð¡¤°Ê²¼¤Ï²Ã»»¼°¤Î·¿ÉÕ¤±µ¬Â§¤Ç¤¢¤ë¡¥ [T-Plus] Γ⊢e_1 : intΓ⊢e_2 : int Γ⊢e_1 + e_2 : int ¤³¤Î¡¤·¿ÉÕ¤±µ¬Â§¤Îľ´¶Åª¤Ê°ÕÌ£(ÆɤßÊý)¤Ï¡¤
Á°Äó¤Î·¿È½ÃǤ¬Á´¤ÆƳ½Ð¤Ç¤¤¿¤Ê¤é¤Ð¡¤·ëÏÀ¤Î·¿È½ÃǤòƳ½Ð¤·¤Æ¤è¤¤
¤È¤¤¤¦¤³¤È¤Ç¤¢¤ë¡¥·¿È½ÃǤϡ¤¶ñÂÎŪ¤Ê·¿´Ä¶¡¤¼°¡¤·¿¤Ë´Ø¤·¤Æ¡¤Æ³½Ð¤¹¤ë¤â ¤Î¤Ê¤Î¤Ç¡¤¤è¤ê¸·Ì©¤Ë¤Ï¡¤µ¬Â§¤ò»È¤¦¤È¤¤¤¦¾ì¹ç¤Ë¤Ï¡¤¤Þ¤º¡¤µ¬Â§¤Ë¸½¤ì¤ë¡¤ Γ, e1 ¤Ê¤É¤Î¥á¥¿ÊÑ¿ô¤ò¼ÂºÝ¤Î·¿´Ä¶¡¤¼°¤Ê¤É¤Ç¶ñÂ⽤·¤Æ»È ¤ï¤Ê¤±¤ì¤Ð¤¤¤±¤Ê¤¤¡¥Î㤨¤Ð¡¤∅ ⊢ 1 : int ¤È¤¤¤¦·¿È½ ÃǤ¬´û¤ËƳ½Ð¤µ¤ì¤Æ¤¤¤¿¤È¤·¤¿¤é(∅ ¤Ï¶õ¤Î·¿´Ä¶¤òɽ¤¹)¡¤¤³¤Î µ¬Â§¤Î Γ ¤ò ∅ ¤Ë¡¤e1, e2 ¤ò¤È¤â¤Ë¡¤ 1¤Ë¶ñÂ⽤¹¤ë¤³¤È¤Ë¤è¤Ã¤Æ¡¤µ¬Â§¤Î¥¤¥ó¥¹¥¿¥ó¥¹¡¤¶ñÂÎÎã(instance) [T-Plus] ∅⊢1 : int∅⊢1 : int ∅⊢1+1 : int ¤¬ÆÀ¤é¤ì¤ë¡¥¤½¤³¤Ç¡¤¤³¤Î¶ñÂ⽤µ¤ì¤¿µ¬Â§¤ò»È¤¦¤È¡¤·¿È½ÃÇ∅ ⊢ 1+1 : int ¤¬Æ³½Ð¤Ç¤¤ë¡¥¤Á¤Ê¤ß¤Ë¡¤°ìÈ̤˲¿¤â¤Ê¤¤¤È¤³¤í¤«¤é¡¤¤¢ ¤ë·¿È½ÃǤòƳ½Ð¤¹¤ë¤Ë¤Ï¡¤Á°Äó¤¬Ìµ¤¤·¿ÉÕ¤±µ¬Â§¤«¤é»Ï¤á¤ë¤³¤È¤Ë¤Ê¤ë¡¥
°Ê²¼¤Ë¡¤ML2¤Î·¿ÉÕ¤±µ¬Â§¤ò¼¨¤¹¡¥ [T-Var] (Γ(x) = τ) Γ⊢x : τ [T-Int] Γ⊢n : int [T-Bool] (b = true ¤Þ¤¿¤Ï b = false) Γ⊢b : bool [T-Plus] Γ⊢e_1 : intΓ⊢e_2 : int Γ⊢e_1 + e_2 : int [T-Mult] Γ⊢e_1 : intΓ⊢e_2 : int Γ⊢e_1 * e_2 : int [T-Lt] Γ⊢e_1 : intΓ⊢e_2 : int Γ⊢e_1 < e_2 : bool [T-If] Γ⊢e_1 : boolΓ⊢e_2 : τΓ⊢e_3 : τ Γ⊢if e_1 then e_2 else e_3 : τ [T-Let] Γ⊢e_1 : τ_1 Γ, x:τ_1 ⊢e_2 : τ_2 Γ⊢let x = e_1 in e_2 : τ_2 µ¬Â§T-Let¤Ë¸½¤ì¤ë Γ, x:τ ¤Ï Γ ¤Ë x ¤Ï τ ¤Ç¤¢¤ë¤È¤¤¤¦¾ðÊó¤ò²Ã¤¨¤¿³ÈÄ¥¤µ¤ì¤¿·¿´Ä¶¤Ç¡¤¤è¤ê¸·Ì©¤ÊÄêµÁ¤È ¤·¤Æ¤Ï¡¤
|
¤È½ñ¤¯¤³¤È¤¬¤Ç¤¤ë¡¥(dom(Γ)¤ÏΓ¤ÎÄêµÁ°è¤òɽ¤¹¡¥)µ¬Â§ ¤ÎÁ°Äó¤È¤·¤Æ³ç¸ÌÆâ¤Ë½ñ¤«¤ì¤Æ¤¤¤ë¤Î¤ÏÉÕÂÓ¾ò·ï(side condition)¤È ¸Æ¤Ð¤ì¤ë¤â¤Î¤Ç¡¤µ¬Â§¤ò»È¤¦ºÝ¤ËÀ®Î©¤·¤Æ¤¤¤Ê¤±¤ì¤Ð¤Ê¤é¤Ê¤¤¾ò·ï¤ò¼¨¤·¤Æ¤¤ ¤ë¡¥
°Ê¾å¤òƧ¤Þ¤¨¤ë¤È¡¤·¿¿äÏÀ¥¢¥ë¥´¥ê¥º¥à¤Î»ÅÍͤϡ¤°Ê²¼¤Î¤è¤¦¤Ë¹Í¤¨¤ë¤³¤È¤¬¤Ç¤¤ë¡¥
ÆþÎÏ: ·¿´Ä¶ Γ ¤È¼° e
½ÐÎÏ: Γ⊢ e : τ ¤È¤¤¤¦·¿È½ÃǤ¬Æ³½Ð¤Ç¤¤ë¤è¤¦¤Ê·¿ τ
¤µ¤Æ¡¤¤³¤Î¤è¤¦¤Ê»ÅÍͤòËþ¤¿¤¹¥¢¥ë¥´¥ê¥º¥à¤ò¡¤¤É¤Î¤è¤¦¤ËÀ߷פ·¤¿¤é¤è¤¤¤Î ¤«¤Ë¤Ä¤¤¤Æ¤Ï¡¤·¿ÉÕ¤±µ¬Â§¤¬»Ø¿Ë¤òÍ¿¤¨¤Æ¤¯¤ì¤ë¡¥¤É¤¦¤¤¤¦¤³¤È¤«¤È¤¤¤¦¤È¡¤ ·¿ÉÕ¤±µ¬Â§¤ò²¼¤«¤é¾å¤ËÆɤळ¤È¤Ë¤è¤Ã¤Æ¥¢¥ë¥´¥ê¥º¥à¤¬ÆÀ¤é¤ì¤ë¤Î¤Ç¤¢¤ë¡¥ Î㤨¤Ð¡¤T-Int ¤ÏÆþÎϼ°¤¬À°¿ô¥ê¥Æ¥é¥ë¤Ê¤é¤Ð¡¤·¿´Ä¶¤Ë´Ø¤ï¤é¤º¡¤ int¤ò½ÐÎϤ¹¤ë¡¤¤ÈÆɤळ¤È¤¬¤Ç¤¤ë¤·¡¤T-Plus¤Ï¡¤Éôʬ¼°¤Î·¿¤òµá¤á ¤Æ¡¤¤½¤ì¤¬Î¾Êý¤È¤â int¤Ç¤¢¤Ã¤¿¾ì¹ç¤Ë¤Ï int·¿¤ò½ÐÎϤ¹¤ë¤ÈÆɤळ¤È¤¬ ¤Ç¤¤ë¡¥
Makefile:
OBJS=syntax.cmo parser.cmo lexer.cmo \ environment.cmo typing.cmo eval.cmo main.cmo
syntax.ml:
type ty = TyInt | TyBool let pp_ty = function TyInt -> print_string "int" | TyBool -> print_string "bool"
main.ml:
open Typing let rec read_eval_print env tyenv = print_string "# "; flush stdout; let decl = Parser.toplevel Lexer.main (Lexing.from_channel stdin) in let ty = ty_decl tyenv decl in let (id, newenv, v) = eval_decl env decl in Printf.printf "val %s : " id; pp_ty ty; print_string " = "; pp_val v; print_newline(); read_eval_print newenv tyenv let initial_tyenv = Environment.extend "i" TyInt (Environment.extend "v" TyInt (Environment.extend "x" TyInt Environment.empty)) let _ = read_eval_print initial_env initial_tyenv
Figure 11: ML2 ·¿¿äÏÀ¤Î¼ÂÁõ (1)
typing.ml:
open Syntax exception Error of string let err s = raise (Error s) (* Type Environment *) type tyenv = ty Environment.t let ty_prim op ty1 ty2 = match op with Plus -> (match ty1, ty2 with TyInt, TyInt -> TyInt | _ -> err ("Argument must be of integer: +")) ... | Cons -> err "Not Implemented!" let rec ty_exp tyenv = function Var x -> (try Environment.lookup x tyenv with Environment.Not_bound -> err ("variable not bound: " ^ x)) | ILit _ -> TyInt | BLit _ -> TyBool | BinOp (op, exp1, exp2) -> let tyarg1 = ty_exp tyenv exp1 in let tyarg2 = ty_exp tyenv exp2 in ty_prim op tyarg1 tyarg2 | IfExp (exp1, exp2, exp3) -> ... | LetExp (id, exp1, exp2) -> ... | _ -> err ("Not Implemented!") let ty_decl tyenv = function Exp e -> ty_exp tyenv e | _ -> err ("Not Implemented!")
Figure 12: ML2 ·¿¿äÏÀ¤Î¼ÂÁõ (2)
¤³¤³¤Ç¤Î¼ÂÁõ¤Î¤¿¤á¤Ë¡¤½¸¹ç±é»»¤ò¼ÂÁõ¤·¤¿ ¥â¥¸¥å¡¼¥ë¤Ç¤¢¤ë MySet (mySet.ml, mySet.mli)¤ò»ÈÍѤ¹¤ë¡¥¤³¤ì¤â¡¤ http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/isle4/src/ ¤«¤é¥À¥¦¥ó¥í¡¼¥É¤·¤Æ¤ª¤¯¤³¤È¡¥
¼¡¤Ë¡¤fun¼°¡¤´Ø¿ôŬÍѼ°
e ::= ⋯ | fun x → e | e1 e2 |
¤Ë¤Ä¤¤¤Æ¹Í¤¨¤ë¡¥´Ø¿ô¤Î·¿¤Ï τ1 → τ2 ¤È¤¹¤ë¤È¡¤ ·¿¤ÎÄêµÁ¤Ï°Ê²¼¤Î¤è¤¦¤ËÊѹ¹¤µ¤ì¤ë¡¥
τ ::= int | bool | τ1 → τ2 |
¤½¤·¤Æ¡¤¤³¤ì¤é¤Î¼°¤Ë´Ø¤·¤Æ·¿ÉÕ¤±µ¬Â§¤Ï°Ê²¼¤Î¤è¤¦¤ËÍ¿¤¨¤é¤ì¤ë¡¥ [T-Abs] Γ, x:τ_1 ⊢e : τ_2 Γ⊢fun x →e : τ_1 →τ_2 [T-App] Γ⊢e_1 : τ_1 →τ_2 Γ⊢e_2 : τ_1 Γ⊢e_1 e_2 : τ_2 µ¬Â§T-Abs¤Ï¡¤´Ø¿ôËÜÂÎ e ¤¬¡¤°ú¿ô x ¤¬ τ1 ¤ò»ý¤Ä¤È¤¤¤¦²¾Äê¤Î ²¼¤Ç τ2 ·¿¤ò»ý¤Ä¤Ê¤é¤Ð¡¤fun x → e ¤Ï τ1 → τ2 ·¿¤Ç¤¢¤ë¡¤¤ÈÆɤá¤ë¡¥¤Þ¤¿¡¤µ¬Â§T-App¤Ï¡¤ e1¤Î·¿¤¬¡¤¤½¤â¤½¤â´Ø¿ô·¿¤Ç¤¢¤ê¡¤¤«¤Ä¡¤¤½¤Î°ú¿ô·¿¤Èe2¤Î·¿¤¬°ì Ãפ·¤Æ¤¤¤ë¾ì¹ç¤Ë¡¤Å¬ÍѼ°Á´ÂΤËe1¤ÎÊÖ¤êÃÍ·¿¤¬¤Ä¤¯¤³¤È¤ò¼¨¤·¤Æ¤¤¤ë¡¥
¤³¤Îµ¬Â§¤Ë¤Ä¤¤¤Æ¡¤Á°Àá¤ÈƱÍͤˡ¤µ¬Â§¤ò²¼¤«¤é¾å¤ËÆɤळ¤È¤Ç¥¢¥ë¥´¥ê¥º¥à¤ò Í¿¤¨¤è¤¦¤È¤¹¤ë¤È T-Abs¤ÇÌäÂ꤬À¸¤¸¤ë¡¥¤È¤¤¤¦¤Î¤â¡¤e ¤Î·¿¤òÄ´ ¤Ù¤è¤¦¤È¤¹¤ë»þ¤Ë x ¤Î·¿¤È¤·¤Æ²¿¤òÍ¿¤¨¤Æ¤è¤¤¤«¤ï¤«¤é¤Ê¤¤¤¿¤á¤Ç¤¢¤ë¡¥ ´Êñ¤ÊÎã¤È¤·¤Æ¡¤fun x → x+1¤È¤¤¤¦¼°¤ò¹Í ¤¨¤Æ¤ß¤è¤¦¡¥¤³¤ì¤Ï¡¤int → int ·¿¤Î´Ø¿ô¤Ç¤¢¤ë¤³¤È¤Ï¡Ö°ìÌÜ¤Ç¡× ¤ï¤«¤ë¤Î¤Ç¡¤°ì¸«¡¤x¤Î·¿¤ò int ¤È¤·¤Æ¿äÏÀ¤ò³¤±¤ì¤Ð¤è¤µ¤½¤¦¤À ¤¬¡¤ÌäÂê¤Ï¡¤ËÜÂμ°¤Ç¤¢¤ëx+1¤ò¸«¤ë¤Þ¤¨¤Ë¤Ï¡¤x ¤Î·¿¤¬ int ¤Ç¤¢¤ë¤³¤È¤¬¤ï¤«¤é¤Ê¤¤¡¤¤È¤¤¤¦¤È¤³¤í¤Ë¤¢¤ë¡¥
¤³¤ÎÌäÂê¤ò²ò·è¤¹¤ë¤¿¤á¤Ë¡¤¡Öº£¤Î¤È¤³¤íÀµÂΤ¬¤ï¤«¤é¤Ê¤¤Ì¤ÃΤη¿¡× ¤òɽ¤¹·¿ÊÑ¿ô(type variable)¤òƳÆþ¤¹¤ë5¡¥
τ ::= α | int | bool | τ1 → τ2 |
¤½¤·¤Æ¡¤·¿¿äÏÀ¥¢¥ë¥´¥ê¥º¥à¤Î½ÐÎϤȤ·¤Æ¡¤ÆþÎÏ(Àµ³Î¤Ë¤Ï·¿´Ä¶Ãæ)¤Ë¸½¤ì¤ë ·¿ÊÑ¿ô¤Î¡ÖÀµÂΤ¬²¿¤«¡×¤òÊÖ¤¹¤³¤È¤Ë¤¹¤ë¡¥¾å¤ÎÎã¤À¤È¡¤¤È¤ê¤¢¤¨¤º x ¤Î·¿¤Ï α ¤Ê¤É¤ÈÃÖ¤¤¤Æ¡¤·¿¿äÏÀ¤ò³¤±¤ë¡¥¿äÏÀ¤Î·ë²Ì¡¤x+1 ¤Î·¿¤Ï int ¤Ç¤¢¤ë¡¤¤È¤¤¤¦¾ðÊó¤Ë²Ã¤¨ α = int ¤È¤¤¤¦¡Ö·¿¿äÏÀ¤Î·ë²Ìα¤Ïint ¤Ç¤¢¤ë¤³¤È¤¬È½ÌÀ¤·¤Þ¤·¤¿¡×¤È¤¤ ¤¦¾ðÊó¤¬Ê֤äƤ¯¤ë¤³¤È¤Ë¤Ê¤ë¡¥ºÇ½ªÅª¤ËT-Abs¤è¤ê¡¤Á´ÂΤη¿¤Ï α → int ¡¤¤Ä¤Þ¤ê¡¤int → int ¤Ç ¤¢¤ë¤³¤È¤¬¤ï¤«¤ë¡¥¤Þ¤¿¡¤fun x → fun y→ x y¤Î¤è¤¦¤Ê¼°¤ò¹Í¤¨¤ë¤È¡¤ °Ê²¼¤Î¤è¤¦¤Ê¼ê½ç¤Ç·¿¿äÏÀ¤¬¤¹¤¹¤à¡¥
¤µ¤é¤Ë¾Ü¤·¤¤¡¤·¿¿äÏÀ¤Î½èÍý¤Ë¤Ä¤¤¤Æ¤Ï¸å½Ò¤¹¤ë¤¬¡¤ ¤³¤³¤ÇÂç»ö¤Ê¤³¤È¤Ï¡¤¤È¤ê¤¢¤¨¤ºÌ¤ÃΤη¿¤È¤·¤ÆÍÑ°Õ¤·¤¿·¿ÊÑ¿ô¤ÎÀµÂÎ ¤¬¡¤¿äÏÀ¤Î²áÄø¤Ç½ù¡¹¤ËÌÀ¤é¤«¤Ë¤Ê¤Ã¤Æ¤¤¤¯¤³¤È¤Ç¤¢¤ë¡¥
¤³¤³¤Þ¤Ç½Ò¤Ù¤¿¤³¤È¤ò¼ÂÁõ¤·¤¿¤Î¤¬¿Þ13¤Ç¤¢¤ë¡¥¤³¤³¤Ç¤Ï·¿ ÊÑ¿ô¤ÏÀ°¿ô¤ò»È¤Ã¤Æɽ¸½¤·¤Æ¤¤¤ë¡¥´Ø¿ô fresh_tyvar ¤Ï fresh_tyvar () ¤È¤¹¤ë¤³¤È¤Ç¡¤¿·¤·¤¤Ì¤»ÈÍѤη¿ÊÑ¿ô¤òÀ¸À®¤¹¤ë¡¥¤³¤ì¤Ï¡¤T-Abs¤Î¤è¤¦ ¤Ë̤ÃΤη¿¤ò¡Ö¤È¤ê¤¢¤¨¤º α ¤È¤ª¤¯¡×ºÝ¤Ë»È¤ï¤ì¤ë¡¥
¾å½Ò¤Î·¿ÊÑ¿ô¤È¤½¤ÎÀµÂΤÎÂбþ´Ø·¸¤ò¡¤·¿ÂåÆþ(type substitution)¤È ¸Æ¤Ö¡¥·¿ÂåÆþ(¥á¥¿ÊÑ¿ô¤È¤·¤Æ S¤ò»ÈÍѤ¹¤ë¡¥)¤Ï¡¤·¿ÊÑ¿ô¤«¤é ·¿¤Ø¤Î(͸Â)¼ÌÁü¤È¤·¤Æɽ¤µ¤ì¤ë¡¥°Ê²¼¤Ç¤Ï¡¤ Sτ ¤Ç τ Ãæ ¤Î·¿ÊÑ¿ô¤ò S ¤ò»È¤Ã¤ÆÃÖ¤´¹¤¨¤¿¤è¤¦¤Ê·¿¡¤ SΓ ¤Ç¡¤ ·¿´Ä¶Ãæ¤ÎÁ´¤Æ¤Î·¿¤Ë S ¤òŬÍѤ·¤¿¤è¤¦¤Ê·¿´Ä¶¤òɽ¤¹¡¥ Sτ¡¤ SΓ ¤Ï¤è¤ê¸·Ì©¤Ë¤Ï°Ê²¼¤Î¤è¤¦¤ËÄêµÁ¤µ¤ì¤ë¡¥
|
·¿ÂåÆþ¤ò»È¤Ã¤Æ¡¤¿·¤·¤¤·¿¿äÏÀ¥¢¥ë¥´¥ê¥º¥à¤Î»ÅÍͤϰʲ¼¤Î¤è¤¦¤ËÍ¿¤¨¤é¤ì¤ë¡¥
ÆþÎÏ: ·¿´Ä¶ Γ ¤È¼° e
½ÐÎÏ: SΓ⊢ e : τ ¤ò·ëÏÀ¤È¤¹¤ëȽÃǤ¬Â¸ºß¤¹¤ë¤è¤¦¤Ê·¿ τ ¤ÈÂåÆþ S
val freevar_ty : ty -> tyvar MySet.t¤È¤¹¤ë¡¥·¿ 'a MySet.t ¤Ï(¼Â¸³WWW¥Ú¡¼¥¸¤Ë¤¢¤ë) mySet.mli ¤ÇÄêµÁ¤µ¤ì ¤Æ¤¤¤ë'a¤òÍ×ÁǤȤ¹¤ë½¸¹ç¤òɽ¤¹·¿¤Ç¤¢¤ë¡¥
type subst = (tyvar * ty) list val subst_type : subst -> ty -> ty·¿ÂåÆþ¤òɽ¤¹·¿ subst ¤Ï·¿ÊÑ¿ô¤È·¿¤Î¤Î¥Ú¥¢¤Î¥ê¥¹¥È [(id1,ty1); ...; (idn,tyn)] ¤Çɽ¸½¤¹¤ë¡¥¤³¤Î¥ê¥¹¥È¤Ï [idn ↦ tyn] ∘ ⋯ ∘[id1 ↦ ty1] ¤È¤¤¤¦·¿ÂåÆþ¤ò ɽ¤¹¡¥½çÈÖ¤¬È¿Å¾¤·¤Æ¤¤¤ë¤³¤È¡¤¤Þ¤¿¡¤ÂåÆþ¤Î¹çÀ®¤òɽ¤¹¤Î¤Ç¡¤ty1 ¤Ë¸½¤ì ¤ë·¿ÊÑ¿ô¤Ï¸å³¤Î¥ê¥¹¥È¤Îɽ¤¹·¿ÂåÆþ¤Î±Æ¶Á¤ò¼õ¤±¤ë¤³¤È¤ËÃí°Õ¤¹¤ë¤³¤È¡¥
Î㤨¤Ð¡¤
let alpha = fresh_tyvar () in subst_type [(alpha, TyInt)] (TyFun (alpha, TyBool))
¤ÎÃÍ¤Ï TyFun (TyInt, TyBool) ¤Ë¤Ê¤ê¡¤
let alpha = fresh_tyvar () in let beta = fresh_tyvar () in subst_type [(beta, (TyFun (TyVar alpha, TyInt))); (alpha, TyBool)] (TyVar beta)
¤ÎÃÍ¤Ï TyFun (TyBool, TyInt) ¤Ë¤Ê¤ë¡¥
Makefile:
OBJS=mySet.cmo syntax.cmo parser.cmo lexer.cmo \ environment.cmo eval.cmo main.cmo
syntax.ml:
... type tyvar = int type ty = TyInt | TyBool | TyVar of tyvar | TyFun of ty * ty (* pretty printing *) let pp_ty = ... let fresh_tyvar = let counter = ref 0 in let body () = let v = !counter in counter := v + 1; v in body let rec freevar_ty ty = ... (* ty -> tyvar MySet.t *)
Figure 13: ML3 ·¿¿äÏÀ¤Î¼ÂÁõ(1)
·¿ÉÕ¤±µ¬Â§¤òį¤á¤Æ¤ß¤ë¤È¡¤T-If¤äT-Plus¤Ê¤É¤Î µ¬Â§¤Ï¡Ö¾ò·ï¼°¤Î·¿¤Ï bool¤Ç¤Ê¤¯¤Æ¤Ï¤Ê¤é¤Ê¤¤¡×¡ÖthenÀá¤È elseÀá¤Î¼°¤Î·¿¤Ï°ìÃפ·¤Æ¤¤¤Ê¤±¤ì¤Ð¤Ê¤é¤Ê¤¤¡×¡Ö°ú¿ô¤Î·¿¤Ï int¤Ç ¤Ê¤¯¤Æ¤Ï¤Ê¤é¤Ê¤¤¡×¤È¤¤¤¦À©Ìó¤ò²Ý¤·¤Æ¤¤¤ë¤³¤È¤¬¤ï¤«¤ë¡¥ML2¤ËÂФ¹ ¤ë·¿¿äÏÀ¤Ç¤Ï¡¤... = TyInt ¤È¤¤¤Ã¤¿·¿(ÄêµÁ¤µ¤ì¤ë¸À¸ì¤Î·¿¤òɽ¸½¤·¤¿ÃÍ) ¤ÎÈæ³Ó¤ò¹Ô¤¦¤³¤È¤Ç¡¤¤³¤¦¤¤¤Ã¤¿À©Ìó¤¬Ëþ¤¿¤µ¤ì¤Æ¤¤¤ë¤³¤È¤ò¸¡ºº¤·¤Æ¤¤¤¿¡¥
¤·¤«¤·¡¤Éôʬ¼°¤Î·¿¤È¤·¤Æ¡¤·¿ÊÑ¿ô¤¬´Þ¤Þ¤ì¤ë²ÄǽÀ¤¬¤Ç¤Æ¤¯¤ë¤¿¤á¡¤ ¤½¤¦¤¤¤Ã¤¿À©Ìó¤Î¸¡ºº¤Ë¤Ï¡¤¤³¤Î¤è¤¦¤Êñ½ãÈæ³Ó¤ÏÉÔ½½Ê¬¤Ç¤¢¤ë¡¥ Î㤨¤Ð¡¤fun x → 1+x ¤È¤¤¤¦¼°¤Î·¿¿äÏÀ²áÄø ¤ò¹Í¤¨¤Æ¤ß¤ë¡¥¾å¤Ç½Ò¤Ù¤¿¤è¤¦¤Ë¡¤¤Þ¤º¡¤x ¤Î·¿¤ò·¿ÊÑ¿ô α ¤È¤ª¤¤¤Æ¡¤1+x¤Î·¿¿äÏÀ¤ò¤¹¤ë¤³¤È¤Ë¤Ê¤ë¡¥ ¤Þ¤º¡¤Éôʬ¼°¤Î·¿¿äÏÀ¤ò¤¹¤ë¤ï¤±¤À¤¬¡¤¤³¤Î¾ì¹ç¡¤¤½¤ì¤¾¤ì¤ÎÉôʬ¼° 1, x¤Î·¿¤Ï¡¤ int¤È α ¤È¤Ê¤ë¡¥¤·¤«¤·¡¤¸å¼Ô¤Î·¿¤¬ int¤Ç¤Ï¤Ê¤¤(ñ½ãÈæ ³Ó¤Ë¼ºÇÔ¤¹¤ë)¤«¤é¤È¤¤¤Ã¤Æ¡¤¤³¤Î¼°¤Ë·¿¤¬¤Ä¤«¤Ê¤¤¤ï¤±¤Ç¤Ï¤Ê¤¤¡¥ ¤³¤³¤Ç¤ï¤«¤ë¤³¤È¤Ï¡Ö̤ÃΤÀ¤Ã¤¿α¤Ï¼Â¤Ïint ¤Ç¤¢¤ë¡× ¤È¤¤¤¦¤³¤È¤Ç¤¢¤ë¡¥¤Ä¤Þ¤ê¡¤·¿¤Ë´Ø¤¹¤ëÀ©Ìó¤ò²Ý¤·¤Æ¤¤¤ëÉôʬ¤Ç̤ÃΤη¿¤Î ÀµÂΤ¬µá¤Þ¤ë¤Î¤Ç¤¢¤ë¡¥¤³¤ÎÎã¤Î¾ì¹ç¤Î½èÍý¤Ïñ½ã¤À¤¬¡¤ T-If¤ÇthenÀá¤ÈelseÀá¤Î¼°¤Î·¿¤¬°ìÃפ¹¤ë¤³¤È¤ò ¸¡ºº¤¹¤ë¤¿¤á¤Ë¤Ï¡¤¤è¤ê°ìÈÌŪ¤Ê¡¤
Í¿¤¨¤é¤ì¤¿·¿¤Î¥Ú¥¢¤Î½¸¹ç {(τ11, τ12), …, (τn1, τn2)} ¤ËÂФ·¤Æ¡¤ S τ11 = Sτ12, …, S τn1 = Sτn2 ¤Ê ¤ë S ¤òµá¤á¤ë
¤È¤¤¤¦ÌäÂê¤ò²ò¤«¤Ê¤±¤ì¤Ð¤¤¤±¤Ê¤¤¡¥¤³¤Î¤è¤¦¤ÊÌäÂê¤Ïñ°ì²½(unification)ÌäÂê¤È¸Æ¤Ð¤ì¡¤·¿¿äÏÀ¤À¤±¤Ç¤Ï¤Ê¤¯¡¤ ·×»»µ¡¤Ë¤è¤ë¼«Æ°¾ÚÌÀ¤Ê¤É¤Ë¤ª¤±¤ë´ðËÜŪ¤ÊÌäÂê¤È¤·¤ÆÃΤé¤ì¤Æ¤¤¤ë¡¥
Î㤨¤Ð¡¤α, int ¤Ï S(α) = int ¤Ê¤ë ·¿ÂåÆþ S¤Ë¤è¤êñ°ì²½¤Ç¤¤ë¡¥¤Þ¤¿¡¤α → bool ¤È (int → β) → β ¤Ï S(α) = int → bool ¤«¤Ä S(β) = bool ¤Ê¤ë S ¤Ë¤è¤êñ°ì²½¤Ç¤¤ë¡¥
ñ°ì²½ÌäÂê¤Ï¡¤ÂоÝ(¤³¤³¤Ç¤Ï·¿)¤Î¹½Â¤¤äÊÑ¿ô¤ÎÆ°¤¯ÈϰϤˤè¤Ã¤Æ¤Ï¡¤ Èó¾ï¤ËÆñ¤·¤¯¤Ê¤ë¤¬¡¤¤³¤³¤Ç¤Ï¡¤·¿¤¬Ã±½ã¤ÊÌÚ¹½Â¤¤ò»ý¤Á¡¤·¿ÂåÆþ¤âñ¤Ë ·¿ÊÑ¿ô¤Ë·¿¤ò³äÅö¤Æ¤ë¤À¤±¤Î¤â¤Î(°ì³¬¤Îñ°ì²½(first-order unification)¤È¸Æ¤Ð¤ì¤ë)¤Ê¤Î¤Ç¡¤²ò¤Ç¤¢¤ë·¿ÂåÆþ¤òµá¤á¤ë¥¢¥ë¥´¥ê¥º¥à¤¬ ¸ºß¤¹¤ë¡¥(¤·¤«¤â¡¤µá¤Þ¤ë·¿ÂåÆþ¤¬¤¢¤ë°ÕÌ£¤Ç¡ÖºÇ¤âÎɤ¤¡×²ò¤Ç¤¢¤ë¤³¤È¤¬ ¤ï¤«¤Ã¤Æ¤¤¤ë¡¥)·¿¤Î¥Ú¥¢¤Î½¸¹ç¤òÆþÎϤȤ··¿ÂåÆþ¤òÊÖ¤¹¡¤Ã±°ì²½¤Î¥¢¥ë¥´¥ê¥º¥à ¤Ï¡¤°Ê²¼¤Î¤è¤¦¤ËÍ¿¤¨¤é¤ì¤ë¡¥ (X⊎ Y ¤Ï¡¤X∩ Y = ∅ ¤Î¤È¤¤Î X ¤È Y ¤ÎϽ¸¹ç¤ò¼¨¤¹¡¥)
|
∅ ¤Ï¶õ¤Î·¿ÂåÆþ¤òɽ ¤·¡¤[α↦τ]¤Ï α¤ò τ ¤Ë¼Ì¤¹¤À¤±¤Î·¿ÂåÆþ ¤Ç¤¢¤ë¡¥¤Þ¤¿FTV(τ)¤Ï τÃæ¤Ë¸½¤ì¤ë·¿ÊÑ¿ô¤Î½¸¹ç¤Ç¤¢¤ë¡¥2ÈÖ ÌÜ¡¤3ÈÖÌܤμ°¤Ï α ¤Ë¤Ä¤¤¤Æ²ò¤±¤¿¤Î¤Ç¡¤¤½¤Î·ë²Ì¤ò»Ä¤ê¤ÎÊýÄø¼°¤Ë ŬÍѤ·¤Æ¤µ¤é¤Ë¤½¤ì¤é¤ò²ò¤Â³¤±¤ë(ñ°ì²½¤ò»î¤ß¤ë)¤³¤È¤ò¼¨¤·¤Æ¤¤¤ë¡¥
val unify : (ty * ty) list -> subst¤È¤·¤Æ¼ÂÁõ¤»¤è¡¥
°Ê¾å¤òÁí¹ç¤¹¤ë¤È¡¤ML3¤Î¤¿¤á¤Î·¿¿äÏÀ¥¢¥ë¥´¥ê¥º¥à¤¬ÆÀ¤é¤ì¤ë¡¥ Î㤨¤Ð¡¤e1+e2 ¼°¤ËÂФ¹¤ë·¿¿äÏÀ¤Ï¡¤T-Plusµ¬Â§¤ò ²¼¤«¤é¾å¤ËÆɤó¤Ç¡¤
¤È¤Ê¤ë¡¥Éôʬ¼°¤Î·¿¿äÏÀ¤ÇÆÀ¤é¤ì¤¿·¿ÂåÆþ¤òÊýÄø¼°¤È¤ß¤Ê¤·¤Æ¡¤ºÆ¤Óñ°ì²½¤ò ¹Ô¤¦¤Î¤Ï¡¤¤Ò¤È¤Ä¤ÎÉôʬ¼°¤«¤é [α ↦ τ1]¡¤¤â¤¦¤Ò¤È¤Ä¤« ¤é¤Ï [α ↦ τ2] ¤È¤¤¤¦ÂåÆþ¤¬ÆÀ¤é¤ì¤¿»þ ¤Ëτ1 ¤È τ2 ¤ÎÀ°¹çÀ¤¬¼è¤ì¤Æ¤¤¤ë¤«(ñ°ì²½¤Ç¤¤ë¤«)¤ò¸¡ºº ¤¹¤ë¤¿¤á¤Ç¤¢¤ë¡¥
typing.ml:
let rec unify = ... (* eqs_of_subst : subst -> (ty * ty) list ·¿ÂåÆþ¤ò·¿¤ÎÅù¼°½¸¹ç¤ËÊÑ´¹ *) let eqs_of_subst s = ... let ty_prim op ty1 ty2 = match op with Plus -> ([(ty1, TyInt), (ty2, TyInt)], TyInt) | ... let rec ty_exp tyenv = function Var x -> (try ([], Environment.lookup x tyenv) with Environment.Not_bound -> err ("variable not bound: " ^ x)) | ILit _ -> ([], TyInt) | BLit _ -> ([], TyBool) | BinOp (op, exp1, exp2) -> let (s1, ty1) = ty_exp tyenv exp1 in let (s2, ty2) = ty_exp tyenv exp2 in let (eqs3, ty) = ty_prim op ty1 ty2 in let eqs = (eqs_of_subst s1) @ (eqs_of_subst s2) @ eqs3 in let s3 = unify eqs in (s3, subst_type s3 ty) | IfExp (exp1, exp2, exp3) -> ... | LetExp (id, exp1, exp2) -> ... | FunExp (id, exp) -> let domty = TyVar (fresh_tyvar ()) in let s, ranty = ty_exp (Environment.extend id domty tyenv) exp in (subst, TyFun (subst_type s domty, ranty)) | AppExp (exp1, exp2) -> ... | _ -> Error.typing ("Not Implemented!")
Figure 14: ML3 ·¿¿äÏÀ¤Î¼ÂÁõ(2)
Á°Àá¤Þ¤Ç¤Î¼ÂÁõ¤Ç¼Â¸½¤µ¤ì¤ë·¿(¥·¥¹¥Æ¥à)¤ÏñÁêŪ¤Ç¤¢¤ê¡¤¤Ò¤È¤Ä¤ÎÊÑ¿ô¤ò ¤¢¤¿¤«¤âÊ£¿ô¤Î·¿¤ò»ý¤Ä¤è¤¦¤Ë°·¤¨¤Ê¤¤¡¥Î㤨¤Ð¡¤
let f = fun x → x in if f true then f 2 else 3;;
¤Î¤è¤¦¤Ê¥×¥í¥°¥é¥à¤Ï¡¤f ¤¬¡¤if¤Î¾ò·ïÉô¤Ç¤Ïbool → bool ¤È¤·¤Æ¡¤¤Þ¤¿¡¤thenÀá¤Ç¤Ï int → int ¤È¤·¤Æ»È¤ï¤ì¤Æ¤¤ ¤ë¤¿¤á¡¤ ·¿¿äÏÀ¤Ë¼ºÇÔ¤·¤Æ¤·¤Þ¤¦¡¥ËÜÀá¤Ç¤Ï¡¤ ¾åµ¤Î¥×¥í¥°¥é¥à¤Ê¤É¤ò¼õÍý¤¹¤ë¤è¤¦ let ¿Áê¤ò¼ÂÁõ¤¹¤ë¡¥
Objective Caml ¤Ç let f = fun x -> x;; ¤È¤¹¤ë¤È¡¤¤½¤Î·¿¤Ï 'a -> 'a ¤Ç¤¢¤ë ¤Èɽ¼¨¤µ¤ì¤ë¡¥¤·¤«¤·¡¤¤³¤³¤Ç¸½¤ì¤ë·¿ÊÑ¿ô 'a ¤Ï¡¤¸å¤Ç¤½¤ÎÀµÂΤ¬È½ÌÀ¤¹ ¤ë(º£¤Î¤È¤³¤í¤Ï)̤ÃΤη¿¤òɽ¤·¤Æ¤¤¤ë¤ï¤±¤Ç¤Ï¤Ê¤¯¡¤¡Ö¤É¤ó¤Ê·¿¤Ë¤Ç¤âÃÖ¤ ´¹¤¨¤Æ¤è¤¤¡×¤³¤È¤ò¼¨¤¹¤¿¤á¤Î¡¤¤¤¤ï¤Ð¡Ö·ê¥Ü¥³¡×¤Ë¤Ä¤±¤¿Ì¾Á°¤Ç¤¢¤ë¡¥¤½¤Î ¤¿¤á¤Ë¡¤'a ¤ò int ¤ÇÃÖ¤´¹¤¨¤Æ int->int ¤È¤·¤Æ °·¤Ã¤ÆÀ°¿ô¤ËŬÍѤȤ·¤¿¤ê¡¤'a ¤òÃÖ¤´¹¤¨¤Æ bool->bool ¤È¤·¤Æ¿¿µ¶ÃÍ ¤ËŬÍѤ·¤¿¤ê¤¹¤ë¤³¤È¤¬¤Ç¤¤ë¡¥¤³¤Î¤è¤¦¤Ê·¿ÊÑ¿ô¤ÎÌò³ä¤Î°ã¤¤¤ò ɽ¤¹¤¿¤á¤Ë¡¤Ç¤°Õ¤Î·¿¤ËÃÖ¤´¹¤¨¤Æ¤è¤¤ÊÑ¿ô¤Ï¡¤·¿¤ÎÁ°¤Ë ∀ α. ¤ò¤Ä¤±¤Æ̤ÃΤη¿¤òɽ¤¹ÊÑ¿ô¤È¶èÊ̤¹¤ë¡¥¤³¤Î¤è¤¦¤Êɽ¸½¤ò ·¿¥¹¥¡¼¥à(type scheme)¤È¸Æ¤Ö¡¥Î㤨¤Ð ∀ α. α → α ¤Ï·¿¥¹¥¡¼¥à¤Ç¤¢¤ë¡¥·¿¤Ï ∀ α. ¤¬¤Ò¤È¤Ä¤â¤Ä¤¤¤Æ¤¤¤Ê¤¤·¿¥¹¥¡¼¥à¤È¹Í¤¨¤é¤ì¤ë¤¬¡¤·¿¥¹¥¡¼¥à¤Ï°ìÈ̤˷¿¤Ç¤Ï¤Ê¤¤¡¥ Î㤨¤Ð¡¤(∀ α.α) → (∀ α.α)¤Î¤è¤¦¤Ê ɽ¸½¤Ï·¿¤È¤Ï¸«Ðö¤µ¤ì¤Ê¤¤¡¥(·¿¥¹¥¡¼¥à¤ò·¿¤È¤·¤Æ°·¤¨¤ë¤è¤¦¤Ê¥×¥í¥°¥é¥ß ¥ó¥°¸À¸ì¤â¸ºß¤¹¤ë¤¬¡¤ÁÇËѤËƱ°ì»ë¤¹¤ë¤È·¿¿äÏÀ¤¬¤Ç¤¤Ê¤¯¤Ê¤Ã¤Æ¤·¤Þ¤¦¡¥) ·¿¥¹¥¡¼¥à¤Ï σ ¤Çɽ¤¹¡¥·¿¤È·¿¥¹¥¡¼¥à¤ÎÄêµÁ¤Ï°Ê²¼¤ÎÄ̤ê¤Ç¤¢¤ë¡¥
|
·¿¥¹¥¡¼¥àÃ桤∀¤Î¤Ä¤¤¤Æ¤¤¤ë·¿ÊÑ¿ô¤ò«Çû¤µ¤ì¤Æ¤¤¤ë¤È¤¤¤¤¡¤ «Çû¤µ¤ì¤Æ¤¤¤Ê¤¤·¿ÊÑ¿ô(¤³¤ì¤é¤Ï̤ÃΤη¿¤òɽ¤¹·¿ÊÑ¿ô¤Ç¤¢¤ë) ¤ò¼«Í³¤Ç¤¢¤ë¡¤¤È¤¤¤¦¡¥ Î㤨¤Ð ∀ α. α → α → β ¤Ë¤ª¤¤¤Æ¡¤ α ¤Ï«Çû¤µ¤ì¤Æ¤ª¤ê¡¤β ¤Ï¼«Í³¤Ç¤¢¤ë¡¥ ¿Þ15¾åȾʬ¤Ë·¿¥¹¥¡¼¥à¤Î¼ÂÁõ¾å¤ÎÄêµÁ¤ò¼¨¤¹¡¥ ´Ø¿ô freevar_tysc ¤Ï·¿¥¹¥¡¼¥à¤«¤é¤½¤ÎÃæ¤Î¼«Í³¤Ê·¿ÊÑ¿ô (¤Î½¸¹ç)¤òµá¤á¤ë´Ø¿ô¤Ç¤¢¤ë¡¥
¼¡¤Ë¡¤·¿¥¹¥¡¼¥à¤ò¤â¤È¤Ë·¿ÉÕ¤±µ¬Â§¤¬¤É¤Î¤è¤¦¤Ë¤Ê¤ë¤«¹Í¤¨¤Æ¤ß¤ë¡¥ ¤Þ¤º¡¤°ìÈÌ¤Ë let ¤ÇÄêµÁ¤µ¤ì¤¿ÊÑ¿ô¤Ï·¿¥¹¥¡¼¥à¤ò»ý¤Ä¤Î¤Ç¡¤ ·¿´Ä¶¤Ï·¿¤«¤é·¿¥¹¥¡¼¥à¤Ø¤Î¼ÌÁü¤È¤Ê¤ë¡¥¤½¤·¤Æ¡¤¤Þ¤º ÊÑ¿ô¤Î·¿ÉÕ¤±µ¬Â§¤Ï°Ê²¼¤Î¤è¤¦¤Ë½ñ¤±¤ë¡¥ [T-PolyVar] (Γ(x) = ∀α_1,…,α_n. τ) Γ⊢x : [α_1↦τ_1,…,α_n↦τ_n]τ ¤³¤Îµ¬Â§¤Ï¡¤ÊÑ¿ô¤Î·¿¥¹¥¡¼¥àÃæ¤Î ∀ ¤Î¤Ä¤¤¤¿·¿ÊÑ¿ô¤ÏǤ°Õ¤Î·¿ ¤ËÃÖ¤´¹¤¨¤Æ¤è¤¤¤³¤È¤ò¡¤·¿ÂåÆþ [α1↦τ1,…,αn↦τn]¤ò»È¤Ã¤Æɽ¸½¤· ¤Æ¤¤¤ë¡¥Î㤨¤Ð¡¤Γ(f) = ∀ α.α → α ¤È¤¹¤ë¤È¡¤
Γ⊢ f : int → int |
¤ä
Γ⊢ f : (int → int ) → (int → int ) |
¤È¤¤¤Ã¤¿·¿È½ÃǤòƳ½Ð¤¹¤ë¤³¤È¤¬¤Ç¤¤ë¡¥¤µ¤Æ¡¤let¤Ë´Ø¤·¤Æ¤Ï¡¤Âç¤Þ¤«¤Ë¤Ï
°Ê²¼¤Î¤è¤¦¤Êµ¬Â§¤Ë¤Ê¤ë¡¥
[T-PolyLet']
Γ⊢e_1 : τ_1 Γ, x:∀α_1.⋯∀α_n. τ_1 ⊢e_2 : τ_2
Γ⊢let x = e_1 in e_2 : τ_2
¤³¤ì¤Ï¡¤e1¤Î·¿¤«¤é·¿¥¹¥¡¼¥à¤òºî¤Ã¤Æ¡¤¤½¤ì¤ò»È¤Ã¤Æ e2 ¤Î
·¿ÉÕ¤±¤ò¤¹¤ì¤Ð¤¤¤¤¤³¤È¤ò¼¨¤·¤Æ¤¤¤ë¡¥¤µ¤Æ¡¤»Ä¤ëÌäÂê¤Ïα1,…,αn
¤È¤·¤Æ¤É¤ó¤Ê·¿ÊÑ¿ô¤òÁª¤Ù¤Ð¤è¤¤¤«¤Ç¤¢¤ë¡¥¤â¤Á¤í¤ó¡¤τ1¤Ë¸½¤ì¤ë
·¿ÊÑ¿ô¤Ë´Ø¤·¤Æ ∀ ¤ò¤Ä¤±¤Æ¡¤¡Ö̤ÃΤη¿¡×¤«¤é¡ÖǤ°Õ¤Î·¿¡×¤Ë
Ìò³äÊѹ¹¤ò¤¹¤ë¤Î¤À¤¬¡¤¤É¤ó¤Ê·¿ÊÑ¿ô¤Ç¤âÊѹ¹¤·¤Æ¤è¤¤¤ï¤±¤Ç¤Ï¤Ê¤¤¡¥
Ìò³äÊѹ¹¤·¤Æ¤è¤¤¤â¤Î¤ÏΓ ¤Ë¼«Í³¤Ë½Ð¸½¤·¤Ê¤¤
¤â¤Î¤Ç¤¢¤ë¡¥Γ Ãæ¤Ë(¼«Í³¤Ë)¸½¤ì¤ë·¿ÊÑ¿ô¤Ï¡¤
¤½¤Î¸å¤Î·¿¿äÏÀ¤Î²áÄø¤ÇÀµÂΤ¬¤ï¤«¤Ã¤ÆÆÃÄê¤Î·¿¤ËÃÖ¤´¹¤¨¤é¤ì¤ë²ÄǽÀ¤¬¤¢¤ë¤Î¤Ç¡¤
Ǥ°Õ¤Ë¤ª¤¤«¤¨¤é¤ì¤ë¤â¤Î¤È¤ß¤Ê¤·¤Æ¤Ï¤Þ¤º¤¤¤Î¤Ç¤¢¤ë¡¥¤È¤¤¤¦¤ï¤±¤Ç¡¤
Àµ¤·¤¤·¿ÉÕ¤±µ¬Â§¤Ï¡¤ÉÕÂÓ¾ò·ï¤ò¤Ä¤±¤Æ¡¤
[T-PolyLet]
Γ⊢e_1 : τ_1 Γ, x:∀α_1.⋯∀α_n. τ_1 ⊢e_2 : τ_2
(α1,…,αn ¤Ï τ1
¤Ë¼«Í³¤Ë½Ð¸½¤¹¤ë·¿ÊÑ¿ô¤Ç Γ ¤Ë¤Ï¼«Í³¤Ë½Ð¸½¤·¤Ê¤¤)
Γ⊢let x = e_1 in e_2 : τ_2
¤È¤Ê¤ë¡¥¿Þ16¤Î´Ø¿ô closure ¤¬¡¤ τ1 ¤È Γ
¤«¤é¾ò·ï¤òËþ¤¿¤¹·¿¥¹¥¡¼¥à¤ò·×»»¤¹¤ë´Ø¿ô¤Ç¤¢¤ë¡¥(ids ¤¬¾å¤Ç¤Î
α1,…,αn¤Ë Âбþ¤¹¤ë¡¥)
·¿¿äÏÀ¤Î²áÄø¤Ë¤ª¤¤¤Æ(·¿´Ä¶Ãæ¤Î)·¿¥¹¥¡¼¥à¤ËÂФ·¤Æ·¿ÂåÆþ¤òºîÍѤµ¤»¤ë¤³ ¤È¤¬¤¢¤ë¡¥¤³¤ÎºÝ¡¤¼«Í³¤Ê·¿ÊÑ¿ô¤È«Çû¤µ¤ì¤¿·¿ÊÑ¿ô¤ò¤È¤â¤Ëtyvar·¿¤ÎÃÍ (¼ÂºÝ¤ÏÀ°¿ô)¤Çɽ¸½¤·¤Æ¤¤¤ë¤¿¤á¤Ë¡¤·¿¥¹¥¡¼¥à¤Ø¤ÎÂåÆþ¤ÎÄêµÁ¤Ï¿¾¯µ¤¤ò¤Ä ¤±¤ëɬÍפ¬¤¢¤ë¡¥¤È¤¤¤¦¤Î¤Ï¡¤ÃÖ¤´¹¤¨¤¿·¿Ãæ¤Î¼«Í³¤Ê·¿ÊÑ¿ô¤È¡¤Â«Çû¤µ¤ì¤Æ ¤¤¤ë·¿ÊÑ¿ô¤¬Æ±¤¸Ì¾Á°¤Çɽ¸½¤µ¤ì¤Æ¤¤¤ë²ÄǽÀ¤¬¤¢¤ë¤¿¤á¤Ç¤¢¤ë¡¥
Î㤨¤Ð¡¤·¿¥¹¥¡¼¥à ∀ α. α → β ¤Ë S(β) = α → int ¤Ç¤¢¤ë¤è¤¦¤Ê·¿ÂåÆþ¤òºîÍѤµ¤»¤ë¤³¤È¤ò¹Í¤¨¤ë¡¥¤³¤ÎÂåÆþ¤Ï¡¤β ¤ò̤ÃΤη¿¤òɽ¤¹ α ¤ò»È¤Ã¤¿·¿¤ÇÃÖ¤´¹¤¨¤ë ¤³¤È¤ò¼¨¤·¤Æ¤¤¤ë¡¥¤·¤«¤·¡¤ÁÇËѤ˷¿¥¹¥¡¼¥àÃæ¤Î β ¤ò ÃÖ¤´¹¤¨¤ë¤È¡¤∀ α.α → α → int ¤È¤¤¤¦·¿¥¹¥¡¼¥à¤¬ÆÀ¤é¤ì¤Æ¤·¤Þ¤¦¡¥¤³¤Î·¿¥¹¥¡¼¥à¤Ç¤Ï¡¤ÂåÆþ¤ÎÁ°¤Ï¡¤ ̤ÃΤη¿¤òɽ¤¹·¿ÊÑ¿ô¤Ç¤¢¤Ã¤¿¡¤ÆóÈÖÌܤÎα¤Þ¤Ç¤¬ Ǥ°Õ¤ËÃÖ¤´¹¤¨¤é¤ì¤ë·¿ÊÑ¿ô¤Ë¤Ê¤Ã¤Æ¤·¤Þ¤Ã¤Æ¤¤¤ë¡¥¤³¤Î¤è¤¦¤Ë¡¤ÂåÆþ¤Ë¤è¤Ã¤Æ ·¿ÊÑ¿ô¤ÎÌò³ä¤¬ÊѲ½¤·¤Æ¤·¤Þ¤¦¤Î¤Ï¤Þ¤º¤¤¤Î¤ÇÈò¤±¤Ê¤±¤ì¤Ð¤¤¤±¤Ê¤¤¡¥
¤³¤Î¤è¤¦¤ÊÊÑ¿ô¤Î¾×ÆÍÌäÂê¤òÈò¤±¤ë¤¿¤á¤Î¡¤¤³¤³¤Ç¼è¤ë²ò·è(²óÈò)ºö¤Ï «ÇûÊÑ¿ô¤Î̾Á°Âؤ¨¡¤¤È¤¤¤¦¼êË¡¤Ç¤¢¤ë6¡¥
¤³¤ì¤Ï¡¤Î㤨¤Ð ∀ α.α → α ¤È ∀β.β → β ¤¬(ʸ»úÎó¤È¤·¤Æ¤Î¸«¤«¤±¤Ï°ã¤Ã¤Æ¤â)°Ọ̃Ū¤Ë¤ÏƱ¤¸·¿¥¹¥¡¼¥à¤òɽ¤·¤Æ¤¤¤ë7¤³¤È¤ò ÍøÍѤ¹¤ë¡¥¤Ä¤Þ¤ê¡¤ÂåÆþ¤¬µ¯¤³¤ëÁ°¤Ë¡¤¿·¤·¤¤·¿ÊÑ¿ô¤ò»È¤Ã¤Æ °ìÀƤË«ÇûÊÑ¿ô¤Î̾Á°¤òÂؤ¨¤Æ¤·¤Þ¤Ã¤Æ¾×Æͤ¬µ¯¤³¤é¤Ê¤¤¤è¤¦¤Ë¤¹¤ë¤Î¤Ç¤¢¤ë¡¥ ¾å¤ÎÎã¤Ê¤é¤Ð¡¤¤Þ¤º¡¤∀ α.α → β ¤ò ∀ γ.γ → β ¤È¤·¤Æ¡¤¤½¤Î¸å¤Ë β ¤ò α → int ¤ÇÃÖ¤´¹¤¨¡¤ ∀ γ.γ → α → int ¤òÆÀ¤ë¤³¤È¤Ë¤Ê¤ë¡¥
¤³¤Î¤è¤¦¤ÊÊÑ¿ô¤Î̾Á°Âؤ¨¤òȼ¤¦ÂåÆþÁàºî¤Î¼ÂÁõ¤ò¿Þ16¤Ë¼¨¤¹¡¥ rename_tysc¡¤subst_tysc ¤¬¤½¤ì¤¾¤ì·¿¥¹¥¡¼¥à¤Î̾Á°Âؤ¨¡¤ÂåÆþ¤Î ¤¿¤á¤Î´Ø¿ô¤Ç¤¢¤ë¡¥
¤³¤³¤Þ¤Ç¤Î¤È¤³¤í¤¬Íý²ò¤Ç¤¤ì¤Ð¡¤¼Â¤Ï·¿¿äÏÀ¥¢¥ë¥´¥ê¥º¥à¼«ÂΤ˴ؤ·¤Æ ±Æ¶Á¤ò¼õ¤±¤ë¤È¤³¤í¤Ï¾¯¤Ê¤¤¡¥¼ÂºÝ¤ËÂ礤ʱƶÁ¤ò¤¦¤±¤ë¤Î¤Ï¡¤ ÊÑ¿ô¤Î½èÍý¤È let ¤Î½èÍý¤Ç¤¢¤ë¡¥ÊÑ¿ô¤Î½èÍý¤Ë´Ø¤·¤Æ¤Ï¡¤·¿ÊÑ¿ô¤ËÂåÆþ¤¹¤ë ·¿(·¿ÉÕ¤±µ¬Â§Ãæ¤Î τ1,…,τn)¤Ï̤ÃΤʤΤǡ¤ ¿·¤·¤¤·¿ÊÑ¿ô¤òÍÑ°Õ¤·¤Æ¤½¤ì¤é¤òÂåÆþ¤¹¤ë¤³¤È¤Ë¤Ê¤ë¡¥(¿Þ16 ¤Î¥³¡¼¥É¤Ç¤Ï¡¤Ì¾Á°Âؤ¨¤Î´Ø¿ô¤òÍøÍѤ·¤Æ¤½¤ì¤ò¼Â¸½¤·¤Æ¤¤¤ë¡¥)
syntax.ml
main.ml
(* type scheme *) type tysc = TyScheme of tyvar list * ty let tysc_of_ty ty = TyScheme ([], ty) let freevar_tysc tysc = ...
... let rec read_eval_print env tyenv = print_string "# "; flush stdout; let decl = Parser.toplevel Lexer.main (Lexing.from_channel stdin) in let (newtyenv, ty) = ty_decl tyenv decl in let (id, newenv, v) = eval_decl env decl in Printf.printf "val %s : " id; pp_ty ty; print_string " = "; pp_val v; print_newline(); read_eval_print newenv newtyenv
Figure 15: ¿ÁêŪlet¤Î¤¿¤á¤Î·¿¿äÏÀ¤Î¼ÂÁõ(1)
typing.ml
type tyenv = tysc Environment.t let rec freevar_tyenv tyenv = ... let closure ty tyenv = let ids = MySet.diff (freevar_ty ty) (freevar_tyenv tyenv) in TyScheme (MySet.to_list ids, ty) ... let rec subst_type subst = ... let rename_tysc tysc = let TyScheme (ids, ty) = tysc in let newids = List.map (fun _ -> fresh_tyvar()) ids in let subst_list = List.map2 (fun id newid -> atomic_subst id (TyVar newid)) ids newids in let subst = List.fold_left (fun s1 s2 -> s1 @@ s2) empty_subst subst_list in TyScheme (newids, subst_type subst ty) let subst_tysc subst tysc = let TyScheme (newids, ty') = rename_tysc tysc in TyScheme (newids, subst_type subst ty') let subst_tyenv subst tenv = ... ... let rec ty_exp tyenv = function Var x -> (try let TyScheme (_, renamed_ty) = rename_tysc (Environment.lookup x tyenv) in (empty_subst, renamed_ty) with Environment.Not_bound -> err ("variable not bound: " ^ x)) | ... let ty_decl tyenv = function Exp e -> let (_, ty) = ty_exp tyenv e in (tyenv, ty) | Decl (id, e) -> ...
Figure 16: ¿ÁêŪlet¤Î¤¿¤á¤Î·¿¿äÏÀ¤Î¼ÂÁõ(2)