Parametric Polymorphism

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

Jacques Garrigue

# 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

ML Edinburgh LCF ML Curry-Howard ML ( ) ( ) ( ) ( ) 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

fp.gby

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

haskell.gby

コンパイラ演習 第 7 回

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

ML 演習 第 4 回

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

cpp1.dvi

monad.gby

つくって学ぶプログラミング言語 RubyによるScheme処理系の実装

Emacs ML let start ::= exp (1) exp ::= (2) fn id exp (3) ::= (4) (5) ::= id (6) const (7) (exp) (8) let val id = exp in

presen.gby

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

Condition DAQ condition condition 2 3 XML key value

untitled

ohp03.dvi

ALG2012-A.ppt

r07.dvi

r03.dvi

ohp07.dvi


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


JavaScript の使い方

untitled

パズルをSugar制約ソルバーで解く

1. A0 A B A0 A : A1,...,A5 B : B1,...,B

ex01.dvi

e ::= c op(e 1,..., e n ) if e 1 then e 2 else e 3 let x = e 1 in e 2 x let rec x y 1... y n = e 1 in e 2 e e 1... e n (e 1,..., e n ) let (x 1,..., x

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

Dive into Algebraic Effects

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

0 1 q

Python Speed Learning

listings-ext

untitled

syspro-0405.ppt

K227 Java 2

ex01.dvi

yacc.dvi

Pascal Pascal Free Pascal CPad for Pascal Microsoft Windows OS Pascal

教室案内.pptx

untitled

Excel97関数編


f(x) x S (optimal solution) f(x ) (optimal value) f(x) (1) 3 GLPK glpsol -m -d -m glpsol -h -m -d -o -y --simplex ( ) --interior --min --max --check -

自己紹介 情報科学の研究をしています 専門はプログラミング言語とか型理論とか 研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらい の著者です

94 expression True False expression FalseMSDN IsNumber WorksheetFunctionIsNumberexpression expression True Office support.office.com/ja-jp/ S

19 3!! (+) (>) (++) (+=) for while 3.1!! (20, 20) (1)(Blocks1.java) import javax.swing.japplet; import java.awt.graphics;

Transcription:

ML 2 2011/04/19

Parametric Polymorphism

Type Polymorphism

?

: val hd_int : int list - > int val hd_bool : bool list - > bool val hd_i_x_b : (int * bool) list - > int * bool etc.

let hd_int = function (x :: _) - > x ;; let hd_bool = function (x :: _) - > x ;; let hd_i_x_b = function (x :: _) - > x ;;?

: hd[α] : α list α hd[int] : int list int hd[bool] : bool list bool hd[int * bool] : (int * bool) list (int * bool) hd[α] OCaml

Parametric Polymorphism Cf. polymorphism ( subtyping polymorphism) Java Cf. overloading (ad- hoc polymorphism) OCaml Haskell type class

: # let id x = x;; val id : 'a - > 'a = <fun> # id 1;; - : int = 1 # id [1; 2; 3];; - : int list = [1; 2; 3] # id (fun x - > x + 1);; - : int - > int = <fun> 'a 'b

: # let fst (x, _) = x;; val fst : 'a * 'b - > 'a = <fun> # let snd (_, x) = x;; val snd : 'a * 'b - > 'b = <fun>

: n # let rec make_list n v = if n = 0 then [] else v :: make_list (n 1) v;; val make_list : int - > 'a - > 'a list = <fun> # make_list 3 1;; - : int list = [1; 1; 1] # make_list 4 "a";; - : string list = ["a"; "a"; "a"; "a"]

fold_left : ('a - > 'b - > 'a) - > 'a - > 'b list - > 'a fold_right : ('a - > 'b - > 'b) - > 'a list - > 'b - > 'b append : 'a list - > 'a list - > 'a list filter : ('a - > bool) - > 'a list - > 'a list split : ('a * 'b) list - > 'a list * 'b list comb : 'a list - > int - > 'a list list

# let id x = x;; val id : 'a - > 'a = <fun> # let id (x : int) = x;; val id : int - > int = <fun> # let id x = (x : int);; val id : int - > int = <fun> # id true;; This expression has type bool but

User- Defined Types

(record) C struct (variant) C enum, union, struct

: type = { 1 : 1 ; 2 : 2 ; } : complex # type complex = { re : float; im : float };; type complex = { re : float; im : float };;

{ 1 = 1 ; 2 = 2 ; } : complex # let c1 = { re = 5.0; im = 3.0 };; val c1 : complex = {re = 5.; im = 3.}

. : # c1.re;; - : float = 5.

# let scalar n { re = r; im = i } = { re = n *. r; im = n *. i };; val scalar : float - > complex - > complex = <fun> # scalar 2.0 { re = 5.0; im = 3.0 };; - : complex = {re = 10.; im = 6.} match with

type = 1 of 1 2 of 2 of 1: bool # type mybool = True False;; type mybool = True False 2: # type value = Int of int Bool of bool;; type value = Int of int Bool of bool

1: mybool # True;; - : mybool = True # False;; - : mybool = False 2: # Int 156;; - : value = Int 156 # Bool false;; - : value = Bool false

: # let not = function True - > False False - > True;; val not : mybool - > mybool = <fun> # not True;; - : mybool = False # not False;; - : mybool = True # let print_value = function Int i - > print_int i Bool b - > print_string (if b then "true" else "false") val print_value : value - > unit = <fun>

: inttree # type inttree = Leaf Node of int * inttree * inttree;; type inttree = Leaf Node of int * inttree * inttree inttree # Leaf;; - : inttree = Leaf # Node (1, Leaf, Leaf);; - : inttree = Node (1, Leaf, Leaf)

: # let rec sum_tree = function Leaf - > 0 Node (v, t1, t2) - > v + sum_tree t1 + sum_tree t2;; val sum_tree : inttree - > int = <fun> # sum_tree (Node(4, Node(5, Leaf, Leaf), Leaf));; - : int = 9

: and # type list = Nil Cons of int * list' and list' = Nil' Cons' of bool * list;; type list = Nil Cons of int * list' and list' = Nil' Cons' of bool * list

Polymorphic Data Type

type inttree = Leaf Node of int * inttree * inttree type booltree = Leaf Node of bool * booltree * booltree type ibtree = Leaf Node of (int * bool) * ibtree * ibtree

: tree[α] = Leaf Node of α * tree[α] * tree[α] tree[int] = Leaf Node of int * tree[int] * tree[int] tree[bool] = Leaf Node of bool * tree[bool] * tree[bool]

: # type 'a tree = Leaf Node of 'a * 'a tree * 'a tree;; type 'a tree = Leaf Node of 'a * 'a tree * 'a tree # Node (5, Leaf, Leaf);; - : int tree = Node (5, Leaf, Leaf) # Node (true, Leaf, Leaf);; - : bool tree = Node (true, Leaf, Leaf) # Leaf;; - : 'a tree = Leaf

type 'a option = None Some of 'a type 'a list = [] (::) of 'a * 'a list

# let div x y = if y = 0 then None else Some (x / y);; val div : int - > int - > int option = <fun> # div 8 2;; - : int option = Some 4 # div 8 0;; - : int option = None

# let rec height = function Leaf - > 0 Node (_, t1, t2) - > 1 + max (height t1) (height t2);; val height : 'a tree - > int = <fun>

# type ('a, 'b) either = L of 'a R of 'b;; type ('a, 'b) either = L of 'a R of 'b # L 1;; - : (int, 'a) either = L 1

ExcepZons

? 0 etc. C++ Java

? (* : raise ( ) *) # let div_e x y = if y = 0 then raise Division_by_zero else x / y;; val div_e : int - > int - > int = <fun> # div_e 8 2;; - : int = 4 # div_e 8 0;; Exception: Division_by_zero.

? (* : try with 1 - > 1 2 - > 2 *) # let div x y = try Some (div_e x y) with Division_by_zero - > None;; val div : int - > int - > int option = <fun> # div 8 2;; - : int option = Some 4 # div 8 0;; - : int option = None

: exception of # exception My_exception;; exception My_exception # My_exception;; - : exn = My_exception # raise My_exception;; Exception: My_exception.

# exception My_int_exception of int;; exception My_int_exception of int # let isprime n = if n <= 0 then raise (My_int_exception n) else ;; val isprime : int - > bool = <fun>

? # exception My_exception;; # exception My_int_exception of int;; # exception My_bool_exception of bool;; # let foo x = try bar x with My_exception - > None My_int_exception i - > Some i with My_bool_exception _ - > None;;

try with try try raise My_exception with My_int_exception i - > Some i with My_exception - > None with with

Programs with Side Effects

?

Unit () : # ();; - : unit = ()

Unit # print_string;; - : string - > unit = <fun> # print_string "Foo\n";; Foo - : unit = () # read_line;; - : unit - > string = <fun> # let s = read_line ();; Bar val s : string = "Bar"

mutable # type bank_account = { name : string; mutable balance : int };; type bank_account = { name : string; mutable balance : int; }

<- (* 1. <- 2 *) # let a = { name = "maeda"; balance = 10000 };; val a : bank_account = {name = "maeda"; balance = 10000} # a.balance;; - : int = 10000 # a.balance <- 20000;; - : unit = () # a.balance;; - : int = 20000 unit

(Reference) C Scheme type 'a ref = { mutable contents : 'a } ( )

# let r = ref 0;; val r : int ref = {contents = 0} #!r;;! - : int = 0 # r := 1;; - : unit = () #!r;; - : int = 1 ref :=

: : 1 ; 2 ; ; n # let t = (print_string "> "; read_line ());; > foo val t : string = "foo"

if else else () (* if then 1 if then 1 else () *) # let r = ref 0;; val r : int ref = {contents = 0} # if!r = 0 then r := 3;; - : unit = () : # r := if!r = 0 then 3;; This expression has type int but is here used with type unit

( ) : # let r1 = ref [];; val r1 : 'a list ref = { contents = [] } # let sum () = fold_right (+) (!r1) 0;; val sum : unit - > int = <fun> # r1 := [true];; - : unit = () # sum ();;??

O'Caml # let r1 = ref [];; val r1 : '_a list ref = { contents = [] } # let sum () = fold_right (+) (!r1) 0;; val sum : unit - > int = <fun> # r1;; - : int list ref = { contents = [] } #!r1 @ [true];; '_a int This expression has type bool but is here used with type int

! f unit 'a 'a f () 'a 'a? let f () = let r = ref None in fun x - > let old = match!r with None - > x Some y - > y in r := Some x; old

OCaml Value restriczon: OK: fun NG: let etc... # (fun () x - > x) ();; - : '_a - > '_a = <fun>

Value restriczon # let f = List.map (fun x - > (x, x));; (* ) val f : '_a list - > ('_a * '_a) list = <fun> : η ( ) # let f xs = List.map (fun x - > (x, x)) xs;; val f : 'a list - > ('a * 'a) list = <fun>

Value restriczon Value restriczon Andrew K. Wright, Maghias Felleisen. A SyntacZc Approach to Type Soundness. Value restriczon O'Caml Jacques Garrigue. Relaxing Value RestricZon. OCaml 3.07

Google Google Scholar ACM Digital Library ( hgp://www.acm.org/ ) ACM CiteSeer.IST ( hgp://citeseerx.ist.psu.edu ) Google Web

2 ( ) : 5/3 13:00

1 (5 ) ('a tree) (preorder) (inorder) (postorder) type 'a tree = Leaf Node of 'a * 'a tree * 'a tree

( ) 1 # preorder (Node(7, Node(5, Node(4, Leaf, Leaf), Leaf), Node(9, Leaf, Node(15, Leaf, Leaf)))) - : int list = [7; 5; 4; 9; 15] 7 5 9 4 15

( ) 1 # inorder (Node(7, Node(5, Node(4, Leaf, Leaf), Leaf), Node(9, Leaf, Node(15, Leaf, Leaf)))) - : int list = [4; 5; 7; 9; 15] 7 5 9 4 15

( ) 1 # postorder (Node(7, Node(5, Node(4, Leaf, Leaf), Leaf), Node(9, Leaf, Node(15, Leaf, Leaf)))) - : int list = [4; 5; 15; 9; 7] 7 5 9 4 15

2 (5 ) type 'a stack = { mutable s : 'a list } val new_stack : unit - > 'a stack (* stack ) val push : 'a stack - > 'a - > unit (* push ) val pop : 'a stack - > 'a (* pop stack Empty_stack )

( ) 2 # let s = new_stack ();; val s : '_a stack = {s = []} # push s 1;; - unit = () # push s 2;; - unit = () # pop s;; - : int = 2 # pop s;; - : int = 1 # pop s;; Exception : Empty_stack.

3 (5 ) 2 let s = new_stack () val s : '_a stack = {s = []} a. 'a stack '_a stack b. '_a stack 'a stack

4 (10 ) O(1) type 'a queue =??? val new_queue : unit - > 'a queue (* queue ) val enqueue : 'a queue - > 'a - > unit (* ) val dequeue : 'a queue - > 'a (* queue Empty_queue )

5 (10 ) f f fix f fix f f (f (f (f (f (f (f...)))))) # let fib = fix (fun g n - > if n <= 2 then 1 else g (n - 1) + g (n - 2));; val fib : int - > int = <fun> # fib 10;; - : int = 55 let rec

6 (10 ) Bool int E V (bool ) V (int ) E V E E + E E E * E E E && E E E = E E E - E E E / E E E E E if E then E else E

6 ( ) V value type value = Bool_value of bool Int_value of int E expr type expr = Const of value Add of expr * expr

6 ( ) (if ((false = true) (2 = 2)) && (3 = 5) then (3 + 5) 9 else 3 * (18 + 20)) + 42 And If Add Or Eq Eq Eq Add Sub Mul Add false true 2 2 3 5 3 5 9 3 18 20 42

7 (15 ) 6 expr eval : expr - > value Bool int Eval_error

8 (20 ) false_t, not_t, and_t, or_t type false_t = B of false_t type 'a not_t = 'a - > false_t type ('a, 'b) and_t = 'a * 'b type ('a, 'b) or_t = L of 'a R of 'b 1 7 let rec let rec?

( ) 8 1. ('a - > 'b) - > ('b - > 'c) - > ('a - > 'c) 2. ('a, ('b, 'c) and_t) or_t - > (('a, 'b) or_t, ('a, 'c) or_t) and_t 3. (('a, 'b) or_t, ('a, 'c) or_t) and_t - > ('a, ('b, 'c) and_t) or_t 4. ('a, 'a not_t) or_t 5. ('a, 'a not_t) and_t 6. 'a - > 'a not_t not_t 7. 'a not_t not_t - > 'a

9 (20 ) O(1) type 'a queue =??? val new_queue : unit - > 'a queue (* queue ) val enqueue : 'a queue - > 'a - > 'a queue (* ) val dequeue : 'a queue - > 'a * 'a queue (* queue Empty_queue )