Objective Caml 3.12 Jacques Garrigue ( ) with Alain Frisch (Lexifi), OCaml developper team (INRIA)

Similar documents
ML Edinburgh LCF ML Curry-Howard ML ( ) ( ) ( ) ( ) 1

jssst-ocaml.mgp

Jacques Garrigue

Parametric Polymorphism

ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1

: gettoken(1) module P = Printf exception End_of_system (* *) let _ISTREAM = ref stdin let ch = ref ( ) let read () = (let c =!ch in ch := inp

Dive into Algebraic Effects

# let rec sigma (f, n) = # if n = 0 then 0 else f n + sigma (f, n-1);; val sigma : (int -> int) * int -> int = <fun> sigma f n ( : * -> * ) sqsum cbsu

# let st1 = {name = "Taro Yamada"; id = };; val st1 : student = {name="taro Yamada"; id=123456} { 1 = 1 ;...; n = n } # let string_of_student {n

ML 演習 第 4 回


ML 演習 第 4 回

2

プログラミング言語 8 字句解析器(lexer)と構文解析器(parser)

2

Clipboard

Terminal ocaml $ ocaml Objective Caml version # 1+2;;<ret> # 1+2;; - : int = 3 ;; OCaml <ret> - : int = 3 OC

SML#³«È¯ºÇÁ°Àþ

Condition DAQ condition condition 2 3 XML key value

「計算と論理」 Software Foundations その3

slide9.dvi

ex01.dvi

Microsoft PowerPoint - ml1.ppt

Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.

コンパイラ演習 第 7 回

プログラミング演習 B ML 編 第 1 回 2015/4/14( コミ ) 2015/4/8( 情報 知能 ) 松田 上野 菊池 ~katsu/proenb2015/ml1.pdf

Java演習(4) -- 変数と型 --

Coq/SSReflect/MathComp による定理証明 サンプルページ この本の定価 判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.

ALG ppt

ex01.dvi

untitled

10/ / /30 3. ( ) 11/ 6 4. UNIX + C socket 11/13 5. ( ) C 11/20 6. http, CGI Perl 11/27 7. ( ) Perl 12/ 4 8. Windows Winsock 12/11 9. JAV

Introduction Purpose This training course demonstrates the use of the High-performance Embedded Workshop (HEW), a key tool for developing software for

Microsoft PowerPoint - ml1.ppt [互換モード]


2018年度「プログラミング言語」配布資料 (10)

橡00horse.PDF

AN 100: ISPを使用するためのガイドライン

koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1

untitled

Ax001_P001_目次-1.ai

橡ボーダーライン.PDF

FA0072 FA0028


DICOM Conformance Statement Carino

untitled

スライド タイトルなし

STARTプログラム.indd

DRT-H64

1st-session key

Microsoft PowerPoint - PC2007.ppt

Copyright c 2008 Zhenjiang Hu, All Right Reserved.

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 (..

2017_Eishin_Style_H01

81

1 I EViews View Proc Freeze

H8.6 P

r03.dvi

「計算と論理」 Software Foundations その4

新・明解Java入門

6-1

listings-ext


人間石川馨と品質管理


ohp03.dvi

1.4操作マニュアル+ユニット解説

0.3% 10% 4% 0.8% 5% 5% 23% 53%

1


- 1 -

%

ID010-2

2

解きながら学ぶC++入門編

Microsoft PowerPoint - lectureNote6.ppt


VB.NETコーディング標準

VDM-SL VDM VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web bool


untitled

第5回東京都廃棄物審議会

西食堂


フィジカルコンディショニング

PowerPoint プレゼンテーション

支援リスト3/30.xls

untitled

programmingII2019-v01

TM-m30 詳細取扱説明書

kyoto.gby

lucene-gosen Solr1

Functional Programming

TM-m30 詳細取扱説明書

ScalaFukuoka 2017 Backlog.key

Microsoft Word - jmanual.doc

取扱説明書の読み替え一覧表

ALG ppt

. IDE JIVE[1][] Eclipse Java ( 1) Java Platform Debugger Architecture [5] 3. Eclipse GUI JIVE 3.1 Eclipse ( ) 1 JIVE Java [3] IDE c 016 Information Pr

3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B

Transcription:

Objective Caml 3.12 Jacques Garrigue ( ) http://www.math.nagoya-u.ac.jp/~garrigue/ with Alain Frisch (Lexifi), OCaml developper team (INRIA)

Jacques Garrigue Modules in Objective Caml 3.12 1 Objective Caml

Jacques Garrigue Modules in Objective Caml 3.12 2 ( val id : a -> a) 3.12 ( )

Jacques Garrigue Modules in Objective Caml 3.12 3 Objective Caml 3.12 open (local open) (local abstract type) (explicit polymorphism annotations) (first-class modules) (signature of a module) (destructive substitution)

Jacques Garrigue Modules in Objective Caml 3.12 4 10 Claudio Russo Moscow ML

Jacques Garrigue Modules in Objective Caml 3.12 5 1 # module type ID = sig val id : a -> a ;; module type ID = sig val id : a -> a # let f id = let module Id = (val id : ID) in (Id.id 1, Id.id true) ;; val f : (module ID) -> int * bool = <fun> # f (module struct let id x = print_line "Id!"; x : ID);; Id! Id! - : int * bool = (1, true)

Jacques Garrigue Modules in Objective Caml 3.12 6 2 module type DEVICE = sig... let devices : (string, (module DEVICE)) Hashtbl.t = Hashtbl.create 17 module PDF = struct... let () = Hashtbl.add devices "PDF" (module PDF: DEVICE)... module Device = (val (try Hashtbl.find devices Sys.argv.(1) with Not_found -> prerr_line "Unknown device"; exit 2) : DEVICE)

Jacques Garrigue Modules in Objective Caml 3.12 7 3 module type PLUGIN = sig type t (* *) val state : t val start : t -> unit val stop : unit -> t ;; let plugins = ref ([] : (string * (module PLUGIN)) list) ;; let new_instance name = let module P = (val List.assoc name!plugins : PLUGIN) in object (* *) val mutable state = P.state method start = P.start state method stop = state <- P.stop () ;; val new_instance : string -> < start : unit; stop : unit > = <fun>

Jacques Garrigue Modules in Objective Caml 3.12 8 4 module type Compute = sig class compute : object method x : int module Default = struct (* *) class compute = object method x = 0 let compute = ref (module Default : Compute) let incr () = (* *) let module M = struct module C = (val!compute : Compute) class compute = object inherit C.compute as super method x = super#x + 1 in compute := (module M : Compute)

Jacques Garrigue Modules in Objective Caml 3.12 9 5 GADTs module TypEq : sig type ( a, b) t (* *) val apply : ( a, b) t -> a -> b val refl : ( a, a) t val sym :... =... module rec Typ : sig module type PAIR = type t and t1 and t2 val eq: (t, t1 * t2) TypEq.t val t1: t1 Typ.typ val t2: t2 Typ.typ type a typ = Int of ( a, int) TypEq.t String of ( a, string) TypEq.t Pair of (module PAIR with type t = a) (* t1 t2... *) = Typ

Jacques Garrigue Modules in Objective Caml 3.12 10 5 GADTs ( )... (* to_string *) let rec to_string : a. a typ -> a -> string = fun (type s) t x -> (* s *) match t with Int eq -> string_of_int (TypEq.apply eq x) String eq -> Printf.sprintf "%S" (TypEq.apply eq x) Pair p -> let module P = (val p : PAIR with type t = s) in let (x1, x2) = TypEq.apply P.eq x in Printf.sprintf "(%s,%s)" (to_string P.t1 x1) (to_string P.t2 x2) Kyseliov ML Workshop 2010

Jacques Garrigue Modules in Objective Caml 3.12 11 OCaml applicative ( ) module type S = sig type t val x : t let r = ref (module struct type t = int let x = 0 : S) module F(X:sig ) = (val!r : S) module A = struct module M = F(A) ;; module M : sig type t = F(A).t val x : t r := (module struct type t = float let x = 0. : S) ;; module N = F(A) ;; module N : sig type t = F(A).t val x : t (* t *) generative ( ) pack unpack

Jacques Garrigue Modules in Objective Caml 3.12 12 (implicit-unpack) module type ID = sig val id : a -> a ;; let f (module Id:ID) = (Id.id 1, Id.id true);; (* unpack *) f (module struct let id x = x );; (* pack *) let rec to_string : a. a typ -> a -> string = fun (type s) (t : s typ) x -> (* *) match t with Int eq -> string_of_int (TypEq.apply eq x) String eq -> Printf.sprintf "%S" (TypEq.apply eq x) Pair (module P) -> (* unpack *) let (x1, x2) = TypEq.apply P.eq x in Printf.sprintf "(%s,%s)" (to_string P.t1 x1) (to_string P.t2 x2) ;;

Jacques Garrigue Modules in Objective Caml 3.12 13 Objective Caml OCaml

Jacques Garrigue Modules in Objective Caml 3.12 14 GADT module rec module rec M : S = M module type of module MyList : sig include module type of List val remove : a -> a list -> a list = struct include List let rec remove a =...

Jacques Garrigue Modules in Objective Caml 3.12 15 2 module type Printable = sig type t val print : t -> unit module type Comparable = sig type t val compare : t -> t -> int module type PrintableComparable = sig (* *) type t val print : t -> unit val compare : t -> t -> int

Jacques Garrigue Modules in Objective Caml 3.12 16 include include module type PrintableComparable = sig include Printable include Comparable with type t = t Error: Multiple definition of the type name t. Names must be unique in a given structure or signature.

Jacques Garrigue Modules in Objective Caml 3.12 17 module type T = sig type t module PrintableF(X:T) = struct module type S = sig val print : t -> unit module ComparableF(X:T) = struct module type S = sig val comparable : t -> t -> int module PrintableComparableF(X:T) = struct module type S = sig include PrintableF(X).S include ComparableF(X).S

Jacques Garrigue Modules in Objective Caml 3.12 18 with module type ComparableInt = Comparable with type t := int ;; module type ComparableInt = sig val compare : int -> int -> int ComparableF(Int).S Comparable ComparableF module ComparableF(X:T) = struct module type S = Comparable with type t := X.t

Jacques Garrigue Modules in Objective Caml 3.12 19 module type PrintableComparable = sig include Printable include Comparable with type t := t module type PrintableInt = (Printable with type t = int) with type t := int module type Printable = sig type printable include Printable with type t := printable

Jacques Garrigue Modules in Objective Caml 3.12 20

Jacques Garrigue Modules in Objective Caml 3.12 21 Objective Caml 3.12 GADTs