Milner Harper LCF ML HOPE (type inference) news letter Polymorphism [28] [30, 24, 13] 3 Standard ML 1990 ML LCF ML The Definition of Standard ML[31] L

Size: px

Start display at page:

Download "Milner Harper LCF ML HOPE (type inference) news letter Polymorphism [28] [30, 24, 13] 3 Standard ML 1990 ML LCF ML The Definition of Standard ML[31] L"

ゆみかあんさい
6 years ago
Views:

1 1 ML ML (Meta Langauge) ML ML LCF LCF (proof ML tactics) ML (higher-order functions) LCF ML ML ML 2 ML 3 ML LCF 4 ML 5 ML Lisp Scheme 6 LCF ML ML 2 ML ML 1970 Edinburgh Edinburgh LCF [12] LCF LCF ML Robin 1

2 Milner Harper LCF ML HOPE (type inference) news letter Polymorphism [28] [30, 24, 13] 3 Standard ML 1990 ML LCF ML The Definition of Standard ML[31] Lisp Standrd ML ( ) ML LCF LCF ML ML LCF ML Cardelli [7] 1980 Edinburgh 3 Standard ML LCF ML Cambridge ML INRIA ML AT&T MacQueen Princeton Appel Standard ML of 1970 Edinburgh New Jersey HOPE [6] Standard ML Milner LCF ML ML The Standard 3 Standard ML ML Core Language [29] Mac- ML Queen HOPE [26] ML [27] Milner Miranda[50] ML Lazy ML[3] Haskell[19] LCF ML ML ML Lisp Standard ML ML 2

3 fn int 1) -> int int int 2) double 3 double 3 3) ML - 113; 113 : int - (2 * 4) * (3 + 5) * 3 + (10-7); 195 : int - val dollar = 108; val dollar = 108 : int * dollar; : int - val double = (fn x => x * 2); val double = fn : int -> int - double 3; 6 : int slanted font fun - fun duplicate x = x^x; val duplicate = fn : string -> string - duplicate "ML"; MLML : string duplicate ^ 2 - ML twice ; val x = E E x - fun twice f x = f (f x); val twice = fn : ( a -> a) -> a -> a ( a -> a) -> a -> a ( a -> a) -> ( a -> a) 3.2 twice a-> a a -> a a twice ML (polymorphic type) fn x => E x x E ( ) twice 3 - twice double 2; 8 : int - val fourtimes = twice double; val fourtimes = fn : int -> int - fourtimes 3; 12 : int

4 twice double 2 ((twice double) 2) datatype a tree twice con Empty : a tree double con Node : ( a * a tree * a tree) -> a tree 2 twice a int * a (int -> int) -> (int-> int) tree Empty a v a tree L, R twice double Node(v,L,R) ML a 2 tree ML Empty - twice duplicate "ML"; Node 2 MLMLMLML : string - val fourth = twice twice; val fourth = fn : ( a -> a) -> a -> a - val T = Node (1,Empty,Empty); - fourth double 2; val T = Node (1,Empty,Empty) : int tree 32 : int Node a sring a int twice twice twice int tree 2 2 = 4 datatype a a -> a ML - fun height Empty = 0 height (Node(x,L,R)) = 1 + max(height L, height R); val height = fn : a tree -> int 3.3 height Empty 0 Node(x,L,R) ML 1 + max(height L, height R) Empty (Node(x,L,R)) datatype a 2 a tree - datatype a tree = Empty Node of ( a * a tree * a tree); height ML 4

5 3.4 handle Find => "illeagal post code"; city name = fn : int -> string zip code data ML find Find city name handle "illeagal post code" tree int 3.5 string 2 Standard ML (int * string) tree find ML ML ML exception raise Standard ML Find - exception Find; - fun find (Empty,key:int ) = raise Find find(node((k,info),t1,t2),key) = if key = k then info else if key < k then find(t2,key) else find(t1,key); val find = fn : ((int*string) tree * int) -> string handle module name.name zip code data open structure 2 1 oepn module name - fun city name zip = find(zip code data,zip) key:int key int = < 5

6 structure Search = struct datatype a tree = Empty Node of a * a tree * a tree exception Find; fun find (Empty,key) = end ML e ::= c x fn x => e e e let x = e in e e fn x => e 1: e fn x => e c x fn x => e e e let x = e 1 in e 2 e 1 x e 2 4 ML ML val x = E; E ML let x = E in E fun let fn ML ML [31] let let let ML ML τ ::= t b τ τ t ML a b int A e A τ ML A e : τ ML 6

7 const A c : τ if c has the type τ var A x : τ if A(x) = τ A{x : τ 1 } e 1 : τ 2 abs A fn x => e 1 : τ 1 τ 2 app A e 1 : τ 1 τ 2 A e 2 : τ 1 app A e 1 e 2 : τ 2 fn x => e 2: ML (1) τ {x:τ} x : τ abs τ fn x => x : τ τ A 1 e 1 : τ 1... A k e k : τ k A e : τ (principal typing) e i A i τ i e A τ 1 e A e : τ e let ML 2 const c var x A x : τ τ {x:τ} x : τ A{x : τ 1 } fn x => x : t t τ abs fn x => x fn x => e 1 A t τ 1 τ 2 e 1 A{x : τ 1 } ( ) τ 2 A{x : τ} A (x) = τ y domain(a) A (y) = A(y) A A 2 e e fn x => e 1 A x x : τ 1 A x τ 1 e 1 7

8 1) A e : σ gen t not free in A A e : t.σ 2) A e : t.σ inst A e : σ[τ/t] A e 1 : σ A{x : σ} e 2 : τ let 3) A let x = e 1 in e 2 : τ 3: ML (2) f x f x Damas Milner {f : t 1 } f : t 1 {x : t 2 } x : t 2 f x σ ::= τ t.σ app 2 t.σ σ t app 3 gen {f : t 1, x : t 2 } f : t 1 {f : t 1, x : t 2 } x : t 2 app t 1, t 2 τ let e x t 1 = t 2 τ inst f x τ t 3 let ID = fn x => x in t 1 t 2 t 3 (ID 3) (ID "ML") f x ID fn x => {f : t 2 t 3, x : t 2 } f x : t x t t 3 t.t t ID 3 t int int -> int Hindley ID "ML" t string string-> string [17] ML Milner let x = e 1 in e 2 let 8

9 1) e 1 τ Standard ML x σ [2] Standard 2) e 2 e 2 ML x 1) σ 6 let Milner ML W Damas Milner C 92% ML 5 ML ML Edinburgh LCF Edinburgh LCF Cambrige CPS LCF [39] Gordon VLSI HOL [11] Constable Nuprl[8] Paulson ML datatype ISSABLE[40] ML ML 5.1 Standard ML of New Jersey MIPS Knuth- ML Bendix ML C 1.6 MacQueen Appel Standard ML 4 Standard Standard ML of New Jersey ML [1, 2] 9

10 ML Milner [28] MacQueen Plotkin Sethi Milner Milner 6 ML [25] ML MacQueen 2 Standard ML [23] [25] Mitchell Harper Standard ML ML [33, 15] ML ML ML ACM Symposium on Principles of Programming Languages ACM Milner Conference on Lisp and Functional Programming Languages ML ACM SIGPLAN ML Tofte [48] Leroy Wise[22] Hoang Mitchell Viswanathan[18] Tofte 6.1 ML ML Milner 6.2 ML [28] Milner ML ML W ML Damas Milner[9] ML ML Milner 4 Damas Milner ML Milner W ML Damas Milner ML ML Wand[51, 52] 10

11 Standard ML of New Jersey Full SML Poly/ML Full SML PoplogML Full SML sml2c Full SML C dtarditi@cs.cmu.edu Edinburgh ML (ftp )ftp.dcs.ed.ac.uk ANU ML mcn@anucsd.anu.edu.au MicroML Caml Light α xavier.leroy@inria.fr 4: ML ML ML Harper [14] [46, 20, 36, 43, 44] [35] ML ML ML [41, 42, 47, 54, 34] [45, 5] Paulson [41] [38] (continuaton) [10], ML [16, 49] [55] [37, 53] [32, 4, 56] [21] Standard ML 5 Standard ML of New Jersey Abstract Hardware Ltd. Poly/ML Standard ML of New Jersey AT&T 7 ML Poly/ML Abstract Hardware Ltd. 4 ML ML (comp.lang.ml) ML ML 2 ML ML ( ) 11

12 [1] Appel, A. W. and MacQueen, D. B. A Standard ML Compiler, Functional Programming Languages and Computer Architecture (LNCS 274) (ed. Kahn, G.), New York (1987), Springer-Verlag. [2] Appel, A. W. and MacQueen, D. B. Standard ML of New Jersey, Third Int l Symp. on Prog. Lang. Implementation and Logic Programming (ed. Wirsing, M.), New York (August 1991), Springer-Verlag, (in press). [3] Augustsson, L. A compiler for Lazy ML, Symposium on LISP and Functional Programming, ACM (1984). [4] Barendregt, H. Lambda calculus with types, Handbook of Logic in Computer Science vol. 2, Oxford University Press (1992). [5] Berry, D., Milner, R. and Turner, D. A Semantics for ML Concurrency Primitives, Proceedings of ACM Symposium on Principles of Programming Languages (1992). [6] Burstall,, MacQueen, and Sannella, HOPE: An experimental applicative language, Proceedings of ACM conference on Lisp and Functional Programming (1980). [7] Cardelli, L. ML under Unix, Polymorphism, 1, 3 (December 1983). [8] Constable, R. L. and et. al., Implementing mathematics with Nuprl proof development system, Prentice-Hall (1988). [9] Damas, L. and Milner, R. Principal type-schemes for functional programs, Proceedings of ACM Symposium on Principles of Programming Languages (1982). [10] Duba, B., Harper, R. and Mac- Queen, D. Typing First-Class Continuations in ML, Eighteenth Annual ACM Symp. on Principles of Prog. Languages, New York (Jan 1991), ACM Press. [11] Gordon, M. J. C. HOL: A proof generating system for higher-order logic, VLSI Specification, Verification and Synthesis (eds. Birtwistle, G. and Subrahmanyam, P. A.), Kluwer Academic Publishing (1988), [12] Gordon, M., Milner, A. and Wadsworth, C. Edinburgh LCF: A Mechanized Logic of Computation, Lecture Note in Computer Science, Springer-Verlag (1979). [13] Harper, R. Standard ML Input/Output, Polymorphism, 2, 2 (October 1985). [14] Harper, R., MacQueen, D. B. and Milner, R. Standard ML, LFCS Report Series ECS-LFCS-86-2, Department of Computer Science, University of Edinburgh (Mar. 1986). [15] Harper, R. and Mitchell, J. C. On the type structure of Standard ML, ACM Transactions on Programming Languages and Systems, 15, 2 (1993), [16] Harper, R., Mitchell, J. C. and E., M. Higher-order modules and the phase distinction, Proceedings of ACM Symposium on Principles of Programming Languages (1990). [17] Hindley, R. The Principal Type-Scheme of an Object in Combinatory Logic, Trans. American Mathematical Society, 146 (Dec. 1969), [18] Hoang, M., Mitchell, J. and Viswanathan, R. Standard ML weak polymorphism and imperative constructs, 12

13 Proc. Logic in Computer Science (to appear) (1993). [19] Hudak, P., Peyton Jones, S., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J., Guzman, M., Hammond, K., Hughes, J., Johnsson, T., Kieburtz, D., Nikhil, R., Partain, W. and Perterson, J. Report on Programming Language Haskel a nonstrict, purely functional language version 1.2, SIGPLAN Notices, Haskel special issue, 27, 5 (1992). [20] Jategaonkar, L. A. and Mitchell, J. ML with extended pattern matching and subtypes, Proc. ACM Conference on LISP and Functional Programming, Snowbird, Utah (July 1988). [21] Leroy, X. and Mauny, M. Dynamics in ML, Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture (1991). [22] Leroy, X. and Weise, P. Polymorphic type inference and assignment, Proceedings of ACM Symposium on Principles of Programming Languages (1991). [23] MacQueen, D. Modules for Standard ML, Proc ACM Conf. on LISP and Functional Programming, New York (1984), ACM Press. [24] MacQueen, D. Modules for Standard ML, Polymorphism, 2, 2 (October 1985). [25] MacQueen, D. Using dependent types to express modular structure, Proceedings of Principles of Programming Languages (Jan. 1986). [26] MacQueen, D. B. Structures and parametarization in a typed functional language, Proc. Symposium on Functional Programming Languages and Computer Architechture, Aspinas, Sweden (1981). [27] MacQueen, D., Plotkin, G. and Seti, R. An ideal model for recursive polymoprphic types, Proceedings of ACM Symposium on Principles of Programming Languages (1984), Extended Version. [28] Milner, R. A Theory of Type Polymorphism in Programming, J. Comput. Syst. Sci., 17 (1978), [29] Milner, R. A proposal for standard ML, Polymorphism, 1, 3 (Dec. 1983). [30] Milner, R. The Standard ML Core Language, Polymorphism, 2, 2 (October 1985). [31] Milner, R., Tofte, M. and Harper, R. The Definition of Standard ML, The MIT Press (1990). [32] Mitchell, J. Type systems for programming languages, Handbook of Theoretical Computer Science (ed. van Leeuwen, J.), MIT Press/Elsevier (1990), chapter chapter 8, [33] Mitchell, J. C. and Harper, R. The Essence of ML, Proceedings of ACM Symposium on Principles of Programming Languages, San Diego, California (Jan. 1988). [34] Myers, C., Clack, C. and Poon, E. Programming with Standard ML, Prentice Hall (1993). [35] Ohori, A. A compilation method for MLstyle polymorphic record calculi, Proceedings of ACM Symposium on Principles of Programming Languages (1992). [36] Ohori, A. and Buneman, P. Type Inference in a Database Programming Language, Proc. ACM Conference on LISP and Functional Programming, Snowbird, Utah (July 1988). [37] Ohori, A. and Buneman, P. Static Type Inference for Parametric Classes, Proceed- 13

14 ings of ACM OOPSLA Conference (1989), Exteded version to apper in Theoretical Aspects of Object-oriented programming, Types, Semantics and Language Design, C. Gunter and J. Mitchell (editors), MIT Press. [38] Ohori, A. and Kato, K. Semantics for Communication Primitives in a Polymorphic Language, Proceedings of ACM Symposium on Principles of Programming Languages (1993). [39] Paulson, L. C. Logic and Computation: Interactive proof with Cambridge LCF, Cambridge University Press (1987). [40] Paulson, L. C. Isabelle: The next 700 theorem prover, Logic and Computer Science (ed. Odifreddi, P.), Academic Press (1990), [41] Paulson, L. C. ML for the Working Programmer, Cambridge University Press (1991). [42] Reade, C. Elements of Functional Programming, Addison-Wesley (1989). [43] Remy, D. Typechecking Records and Variants in a Natural Extension of ML, Proceedings of ACM Symposium on Principles of Programming Languages (1989). [44] Remy, D. Typing Record Concatenation for Free, Proceedings of ACM Symposium on Principles of Programming Languages (1992). [45] Reppy, J. H. CML: A higher-order concurrent language, Proceedings of ACM Conference on Programming Language Design and Implementation (1991). [47] Stansifer, R. ML Primer, Prentice Hall (1992). [48] Tofte, M. Operational Semantics and Polymorphic Type Inference, PhD thesis, Department of Computer Science, University of Edinburgh (1988). [49] Tofte, M. Principal Signatures for Higher-order Program Modules, Proceedings of ACM Symposium on Principles of Programming Languages (1992). [50] Turner, D. Miranda: A non-strict functional language with polymorphic types, Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science 201, Springer-Verlag (1985). [51] Wand, M. Complete Type Inference for Simple Objects, Proceedings of the Second Annual Symposium on Logic in Computer Science, Ithaca, New York (June 1987). [52] Wand, M. Corrigendum : Complete Type Inference for Simple Object, Proceedings of the Third Symposium on Logic in Computer Science (1988). [53] Wand, M. Type Inference for Records Concatenation and Simple Objects, Proceedings of 4th IEEE Symposim on Logic in Computer Science (1989). [54] Wikstrom, A. Functional Programming Using Standard ML, Prentice Hall (1987). [55],.,, 17, (1992). [56] I IV,, 8, 1,2,3,4 (1991), 25 33,40 46,3 8, [46] Stansifer, R. Type Inference with Subtypes, Proceedings of ACM Symposium on Principles of Programming Languages (1988). 14

shift/reset [13] 2 shift / reset shift reset k call/cc reset shift k shift (...) k 1 + shift(fun k -> 2 * (k 3)) k 2 * (1 + 3) 8 reset shift reset (..

shift/reset [13] 2 shift / reset shift reset k call/cc reset shift k shift (...) k 1 + shift(fun k -> 2 * (k 3)) k 2 * (1 + 3) 8 reset shift reset (.. arisa@pllab.is.ocha.ac.jp asai@is.ocha.ac.jp shift / reset CPS shift / reset CPS CPS 1 [3, 5] goto try/catch raise call/cc [17] control/prompt [8], shift/reset [5] control/prompt, shift/reset call/cc (continuationpassing