1, 2 1 m110057@shibaura-it.ac.jp 2 sasano@sic.shibaura-it.ac.jp Eclipse Visual Studio ML Standard ML Emacs 1 ( IDE ) IDE C C++ Java IDE IDE IDE IDE Eclipse Java IDE Java Standard ML 1 print (Int. 1
Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs 2 3 4 5 6 7 8 Standard ML 9 10 11 2 M M ::= x c λx.m M M let x = M in M end (M) x c λx.m M M let x = M in M end let M M M σ := α 1... α n.τ τ := int α τ τ σ τ int α τ 1 τ 2 τ 1 τ 2 σ = α 1... α n.τ 0 τ = [τ 1 /α 1... τ n /α n ]τ 0 τ 1,..., τ n τ σ τ < σ
(const) Γ c : τ (c : τ Const) (var) Γ{x : σ} x : τ if τ < σ (app) Γ M 1 : τ 1 τ 2 Γ M 2 : τ 1 Γ M 1 M 2 : τ 2 (abs) Γ{x : τ 1 } M : τ 2 Γ λx.m : τ 1 τ 2 (let) Γ M 1 : τ 1 Γ{x 1 : Cls(Γ, τ 1 )} M 2 : τ 2 Γ let x 1 = M 1 in M 2 end : τ 2 1. M pre c = {} pre x = {( s, x) s is a prefix of x} pre (M 1 M 2 ) = {(M 1 P 2, x) (P 2, x) pre M 2 } {(P 1, x) (P 1, x) pre M 1 } pre (λx.m) = {(λx.p, x) (P, x) pre M} pre (let x = M 1 in M 2 end) = {(let x = M 1 in P 2, x) (P 2, x) pre M 2 } {(let x = P 1, x) (P 1, x) pre M 1 } pre((m)) = {((P, x) (P, x) pre M} 2. pre M let ML [17] 1 1 (M) Γ M τ Γ M : τ Γ x τ Γ{x : τ} Γ x Γ(x) Cls Γ τ F T V (τ) \ F T V (Γ) = {α 1,..., α n } α 1 α n. τ F T V Const 1 P P ::= λx.p M P let x = M in P let x = P (P f f M P 2 pre pre M M c pre let pre pre M (λabc. abc) 1 pre {((λabc. a, abc), ((λabc. ab, abc), ((λabc. abc, abc)} pre 1 1 ( ) P Γ V v V, M, τ, Γ M : τ, (P, v) pre M V V
P let xx = 1 in let xy = λx.λy.x y in let xz = λx.x in xy x Γ xx xy xz xy xz xx {xy, xz} 3 int αβ. (α β) α β α. α α x xy xy xx x 3 P M M P M [19] 3.1 [19] 3.2 3.1 P M [18] P let ff = λx.+ x 1 in ff ( f + int int int P P end 1 f α α = int int ff ff int int P ff ( f ff ( f [ ]) end [ ] f [ ] α β α = β int ff int int f β int ff f ff
P ff ( f ff ( f [ ] [ ]) end α β int ff 100 3.2 0 3.1 P (let ff = λx.+ x 1 in (ff ( f )) end) ( f ) f, f [ ], f [ ] [ ], f [ ] [ ] [ ] (ff ( f )) ff f, ff ( f [ ]), ff f [ ], ff ( f [ ]) [ ] ff int int ff ff f ff ff ff int int ff ff ff [ ] f ff f int f ff [ ] ff ( f ) int (ff ( f )) int ff f ff ff 4 P P D ::= D λx.d M D let x = D in [ ] end let x = M in D end P D cmp 3
cmp : P D cmp = cmp (λx.p ) = λx.(cmp P ) cmp (M P ) = (M (cmp 2 P )) cmp (let x = M in P ) = (let x = M in cmp P end) cmp (let x = P ) = (let x = cmp P in [ ] end) cmp ((P ) = (cmp P ) cmp 2 : P D cmp 2 = cmp 2 (let x = M in P ) = (let x = M in cmp P end) cmp 2 (let x = P ) = (let x = cmp P in [ ] end) cmp 2 ((P ) = cmp P 3. cmp cmp 2 cmp 2 λx.p M P cmp 2 cmp 2 cmp (λx.p ) (λx.(cmp P )) P cmp P let xa = λx.x 2 in let yy = λx.x in let xc = 3 in xa ( x cmp D (let xa = λx.x 2 in (let yy = λx.x in (let xc = 3 in (xa ( x ) ) end) end) end) 5 D V Milner W [17] 4 V D Γ 3 V Milner W V W W Γ M S τ W S(Γ) M : τ W V W U[18] U ( 1 ) V W W V 3 V W V W V
V(Γ, D) = case D of let N = {count(γ(x)) x dom(γ)} T = {g(x) x N} in {(, τ, (Γ, τ)) τ T } D let {(S 0, τ 0, C 0 ),..., (S i, τ i, C i )} = V(Γ, D) {τ 0,0,..., τ 0,k } = at(τ 0 ). {τ i,0,..., τ i,m } = at(τ i ) in {(S 0, τ 0,0, C 0 ),..., (S 0, τ 0,k, C 0 ),. (S i, τ i,0, C i ),..., (S i, τ i,m, C i )} λx.d let {(S 0, τ 0, C 0 ),..., (S i, τ i, C i )} = V(Γ{x : α}, D) (α fresh) in {(S 0, S 0 (α) τ 0, C 0 ),..., (S i, S i (α) τ i, C i )} M D let (S 1, τ 1 ) = W(Γ, M) {(S 2,0, τ 2,0, C 2,0 ),..., (S 2,i, τ 2,i, C 2,i )} = V(S 1 (Γ), D) S 3,j = U{(S 2,j (τ 1 ), τ 2,j α j )} (α j fresh) (j {0,..., i}) in {(S 3,j S 2,j S 1, S 3,j (α j ), C 2,j ) j {0,..., i}} let x = D in [ ] end let {(S 0, τ 0, C 0 ),..., (S i, τ i, C i )} = V(Γ, D) in {(S 0, α 0, C 0 ),..., (S i, α i, C i )} (α 0,..., α i fresh) let x = M in D end let (S 1, τ 1 ) = W(Γ, M) {(S 2,0, τ 2,0, C 2,0 ),..., (S 2,i, τ 2,i, C 2,i )} = V(S 1 (Γ){x : Cls(S 1 (Γ), τ 1 )}, D) in {(S 2,j S 1, τ 2,j, C 2,j ) j {0,..., i}} count(τ 1 τ 2 ) = count(τ 2 ) + 1 count(α) = 0 count(int) = 0 g(n + 1) = α g(n) (α fresh) g(0) = α (α fresh) at(τ 1 τ 2 ) = {τ 1 τ 2 } at(τ 2 ) at(α) = {α} at(int) = {int} 4. V
D M V 3 [ ] [ ] V D D 0 V D 4 at V τ 1 τ k (τ k int ) τ 1,..., τ k α 1,..., α k α 1 α k count g count τ τ count (int int int) 2 g n n + 1 g(2) α 0 α 1 α 2 α 0, α 1, α 2 count g 1 6 D 2 D 2 τ 0,..., τ i 0 D 0 V 3 V V V(Γ, D) (S, τ, (Γ, τ )) S Γ τ V 4 D V V(, D) D V Γ Γ = {xa : α.(int α) α, yy : α.α α, xc : int} f V x 2 3 {(, β 1 β 2, (Γ, β 1 β 2 )), (, β 3, (Γ, β 3 ))} 1 3 2 β 1 β 2 2 3 2 β 3 at V ( x ) 3 3 {(, β 1 β 2, (Γ, β 1 β 2 )), (, β 2, (Γ, β 1 β 2 )), (, β 3, (Γ, β 3 ))} xa ( x ) V 3 S 1 = U{(int α 0 ) α 0, (β 1 β 2 ) γ 1 )} S 2 = U{(int α 1 ) α 1, β 2 γ 2 )} S 3 = U{(int α 2 ) α 2, β 3 γ 3 )} (int α i ) α i (i = 0, 1, 2) xa α.(int α) α α α 0, α 1, α 2 W γ 1, γ 2, γ 3 V V xa ( f ) 3 3 {(S 1, α 0, (Γ, β 1 β 2 )), (S 2, α 1, (Γ, β 1 β 2 )), (S 3, α 2, (Γ, β 3 ))}
3 3 V(, D) S 1, S 2, S 3 β 1 β 2, β 1 β 2, β 3 3 int α 0, β 1 int α 1, int α 2 S 1, S 2, S 3 Γ Γ V 3 3 6 Γ τ τ α 1... α k.τ [β 1 /α 1 ]... [β k /α k ]τ (β 1,..., β k fresh) 5 int α 0 β 1 int α 1 int α 2 Γ = {xa : α.(int α) α, yy : α.α α, xc : int} xa, yy, xc 3 3 3 = 9 U{(int α 0, (int α 5 ) α 5 )}, U{(int α 0, α 6 α 6 )}, U{(int α 0, int)}, U{(β 1 (int α 1 ), (int α 5 ) α 5 )}, U{(β 1 (int α 1 ), α 6 α 6 )}, U{(β 1 (int α 1 ), int)}, U{(int α 2, (int α 5 ) α 5 )}, U{(int α 2, α 6 α 6 )}, U{(int α 2, int)} 2 4 5 8 2 xa yy xa x yy {xa} 7 1 1 P Γ 5 V {(S 0, τ 0, (Γ, τ 0 )),..., (S i, τ i, (Γ, τ i ))} = V(Γ, cmp P ) V V = { {x x dom(sj (Γ )), j {0,...,i} U{(S j (Γ )(x), S j (τ j ))}, P s s x }} 1 2
1 ( ) 1 V 1 v V, M, τ, Γ M : τ, (P, v) pre M 2 ( ) 1 1 V M, τ, Γ M : τ, (P, v) pre M v V 2 2 V D D 8 Standard ML Emacs lambda-mode Emacs Lambda-mode web http: //www.cs.ise.shibaura-it.ac.jp/complement/ lambda-mode lambda-mode 3 2 3 auto-complete [5] auto-complete 5 x lambda-mode 5. lambda-mode lambda-mode Standard ML 6 let, id, val, in, end, =, =>, fn, (, ), const, ws, EOF
start := exp (1) exp := appexp (2) fn id => exp (3) appexp := atexp (4) appexp atexp (5) atexp := id (6) const (7) (exp) (8) let decseq in exp end (9) dec := val id = exp (10) decseq := dec decseq (11) ɛ (12) 6. id const ws EOF id const 0 0 9 0 const + - ws int + - int int int id id EOF LR [16] yacc kmyacc[8] EOF EOF EOF EOF id 2 id atexp id 4 cmp cmp P D P 1 2 [19] 1 appexp 2 5 2
start exp let decseq in appexp ( dec val id ff = exp decseq atexp id ff fn id x => exp appexp appexp atexp appexp atexp atexp id x const 1 id+ 7. ɛ appexp appexp atexp atexp id let decseq in exp end dec decseq appexp val id ff = exp ɛ appexp atexp fn id x => exp atexp appexp id ff (exp) appexp appexp atexp atexp appexp atexp atexp id atexp id x const 1 id+ 8. 5 appexp ::= appexp atexp appexp ::= appexp atexp appexp mark mark ::= appexp 1 appexp mark mark exp f let val ff = fn x => + x 1 in ff (f_ _ + int int int f let, val, ff, =, fn, id x, =>, id +, id x, const 1, in, ff, (, id, EOF 7 let, decseq, in, appexp, (, appexp 8 8 mark ::= appexp V 4 D 5 6 lambda-mode
9 Lambda-mode CPU Intel Core i7 920 6GB OS Windows 7 Home Premium 64bit Emacs Meadow (GNU Emacs 22.2.1) Let let let 1 1 let 30 1 let 1 1 let let 1 100 let 1 ( ) 10 5 5 50 26 30 100 77 88 1. 10 IDE Visual Studio Intellisense Eclipse content assist [2] vim omni completion intellisense content assist IDE Visual F# Visual C++ Visual C# Eclipse C++ Java Visual Studio
Eclipse FP[4] Haskell Eclipse Leksah[9] Haskell IDE Caml mode [1] tuareg mode [12] Caml OCaml Emacs caml mode OCamlSpotter[11] Java Development Environment for Emacs [7] Java Emacs F# Emacs [6] OCaml Development Tools [10] Eclipse OCaml IDE [13] [14] Djinn[3] [15] 11 1,2 Haskell Standard ML OCaml
Haskell ML [1] Caml mode. http://www.emacswiki.org/emacs/camlmode. [2] Content assist. http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform. doc.isv/guide/editors contentassist.htm. [3] Djinn. http://permalink.gmane.org/gmane.comp.lang.haskell.general/12747. [4] Eclipse FP. http://eclipsefp.sourceforge.net/. [5] EmacsWiki: Auto complete. http://www.emacswiki.org/emacs/autocomplete. [6] Fsharp mode. http://fsharp-mode.sourceforge.net/. [7] Java development environment for Emacs. http://jdee.sourceforge.net/. [8] KMyacc. http://www005.upp.so-net.ne.jp/kmori/kmyacc/. [9] Leksah. http://leksah.org/. [10] OCaml Development Tools. http://ocamldt.free.fr/. [11] OCamlSpotter. http://jun.furuse.info/hacks/ocamlspotter/. [12] Tuareg mode. http://www-rocq.inria.fr/ acohen/tuareg/index.html.en. [13] Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, Vol. 50, pp. 189 224, 2004. [14] Masatomo Hashimoto and Atsushi Ohori. A typed context calculus. Theoretical Computer Science, Vol. 266, No. 1-2, pp. 249 272, 2001. [15] Susumu Katayama. Systematic search for lambda expressions. In Trends in Functional Programming, pp. 111 126, 2005. [16] Donald E. Knuth. On the translation of languages from left to right. Information and Control, Vol. 8, No. 6, pp. 607 639, 1965. [17] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, Vol. 17, No. 3, pp. 348 375, 1978. [18] John A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, Vol. 12, No. 1, pp. 23 41, 1965. [19],. Emacs. 12, pp. 177 190, 2010.