Jacques Garrigue

Size: px

Start display at page:

Download "Jacques Garrigue"

しょうこうすい
4 years ago
Views:

1 Jacques Garrigue

2 Garrigue 1

3 Garrigue 2 $ print_lines () > for i in $1; do > echo $i > done $ print_lines "a b c" a b c

4 Garrigue 3 Emacs Lisp (defun print-lines (lines) (dolist (str lines) (insert str) (insert "\n"))) (print-lines ("a" "b c")) a b c (print-lines (("a") ("b" "c"))) error print-lines

5 Garrigue 4 C #include<stdio.h> void print_lines(char *lines[]) { while (*lines!= NULL) printf("%s\n", *lines++); } int main() { char *lines[] = { "a", "b c", NULL }; print_lines(lines); } $./print_lines a b c

6 Garrigue 5 C #include<stdio.h> void print_lines(char *lines[]) { while (*lines!= NULL) printf("%s\n", *lines++); } int main() { char *lines[] = { "a", "b c", (char*)3, NULL }; print_lines(lines); } $./print_lines a b c Segmentation fault

7 Garrigue 6 C ( lines++) ( (char*)3) struct person { char name[20]; int age; } union person_or_id { struct person *person; int id; }

8 Garrigue 7 1 P P

9 Garrigue Church Turing (Curry-Howard )

10 Garrigue 9 τ ::= b τ τ t ::= x λ(x : τ) t t(t) λ(plus : nat nat nat) λ(y : nat) plus(y)(y)

11 Garrigue 10 Γ ::= {x 1 : τ 1,..., x n : τ n } Γ t τ Γ t : τ x : τ Γ Γ x : τ Γ, x : τ t 1 : τ 1 Γ λ(x : τ) t 1 : τ τ 1 Γ t 1 : τ 2 τ Γ t 2 : τ 2 Γ t 1 (t 2 ) : τ

12 Garrigue 11 v ::= c (η, λ(x : τ) t) η ::= {x 1 v 1,..., x n v n } η = t v η t v x v η η = x v η = λ(x : τ) t (η, λ(x : τ) t) η = t 1 (η, λ(x : τ) t ) η = t 2 v 2 η, x v 2 = t v 3 η = t 1 (t 2 ) v 3

13 Garrigue 12 2 t t : τ t v : = t v

14 Garrigue 13 type a = C 1 of τ τ 1m1 C 2 of τ τ 2m2. C n of τ n1... τ nmn C i a (m i = 0 Γ C i : a ) Γ t 1 : τ i1... Γ t mi : τ imi Γ C i (t 1,..., t mi ) : a

15 Garrigue 14 a b type pair_a_b = Pair_a_b of a * b a type option_a = Some_a of a None a type list_a = Nil Cons of a * list_a [a1; a2; a3] = Cons (a1, Cons (a2, Cons (a3, Nil))) type nat = Zero Succ of nat 3 = Succ (Succ (Succ (Zero)))

16 Garrigue 15 match match t with C 1 (x 1,..., x m1 ) t 1. C n (x n,..., x mn ) t n Γ t : a Γ, x 1 : τ i1,..., x mi : τ imi t i : τ (1 i n) Γ match t with C 1 (x 1,..., x m1 ) t 1... C n (x n,..., x mn ) t n : τ η = t C i (v 1,..., v mi ) η, x 1 v 1,..., x mi v mi = t i v η = match t with C 1 (x 1,..., x m1 ) t 1... C n (x n,..., x mn ) t n v

17 Garrigue 16 OCaml let fst_a_b (p : pair_a_b) = match p with Pair_a_b (a,b) -> a val fst_a_b : pair_a_b -> a let snd_a_b (p : pair_a_b) = match p with Pair_a_b (a,b) -> b val snd_a_b : pair_a_b -> b let rec add (m : nat) (n : nat) = match m with Zero -> n Succ m -> Succ (add (m ) (n)) val add : nat -> nat -> nat

18 Garrigue 17 type ( a, b) pair = Pair of a * b type a option = Some of a None type a list = Nil Cons of a * a list let fst (p : ( a, b) pair) = match p with Pair (a,b) -> a val fst : ( a, b) pair -> a let snd (p : ( a, b) pair) = match p with Pair (a,b) -> b val snd : ( a, b) pair -> b let rec append (l1 : a list) (l2 : a list) = match l1 with None -> l2 Cons (a, l1 ) -> Cons (a, append (l1 ) (l2)) val append : a list -> a list -> a list

19 Garrigue 18 let rec type a recc = In of ( a recc -> a) let out (In x) = x val out : a recc -> a recc -> a let y (f : ( a -> b) -> ( a -> b)) = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a)) val y : (( a -> b) -> a -> b) -> a -> b y

20 Garrigue 19 C OCaml Haskell Damas Milner 3 ( ) P Γ Γ P : τ τ τ τ

21 Garrigue 20 Γ f : α f Γ x : α x Γ g : α g Γ x : α x Γ f(x) : α 2 Γ g(x) : α 3 Γ f(x)(g(x)) : α 1 λf λg λx f(x)(g(x)) : α Γ = f : α f, g : α g, x : α x {α = α f α g α x α 1, α 2 = α 3 α 1, α f = α x α 2, α g = α x α 3 } mgu( ) σ σ(α) = (α x α 3 α 1 ) (α x α 3 ) α x α 1

22 Garrigue 21

23 Garrigue 22 let fst p = match p with Pair (a,b) -> a val fst : ( a, b) pair -> a let snd p = match p with Pair (a,b) -> b val snd : ( a, b) pair -> b let rec append l1 l2 = match l1 with None -> l2 Cons (a, l1 ) -> Cons (a, append l1 l2) val append : a list -> a list -> a list

24 Garrigue 23

25 Garrigue 24 let l = [ Feet 3.0; Mm 33.2 ] val l : [> Feet of float Mm of float ] list let normalize len = match len with Feet n -> Inch (n *. 12.) Inch n -> Inch n Cm n -> Mm (n *. 10.) Mm n -> Mm n val normalize : [< Cm of float Feet of float Inch of float Mm of float ] -> [> Inch of float Mm of float ]

26 Garrigue 25 ( ) ( a list as a) let rec length l = match l with Nil -> 0 Cons (a, t) -> 1 + length t val length : ([< Cons of b * a Nil ] as a) -> int ([ Cons of b * [ Cons of b * a] Nil ] as a)

27 Garrigue 26 (U, L, T ) (Fin(L) L) Fin(L) Fin(L T ) U L [> Feet of float Mm of float ] list = α :: (L, {Feet, Mm}, {Feet float, Mm float}) α list [< C of f F of f I of f M of f ] -> [> I of f M of f ] = α 1 :: ({C, F, I, M},, {C f, F f, I f, M f}), α 2 :: (L, {I, M}, {I f, M f}) α 1 α 2

28 Garrigue 27 mgu mgu {α = [< A of int B], α = [< A of α 1 B]} σ(α 1 ) = int {α = [ B], α 1 = bool} σ = {α [ B]} σ = {α [< A of int & α 1 B]} A α α 1 = int

29 Garrigue 28 LablGL OpenGL 3D C Lisp LablTk Tcl/Tk GUI LablGTK Gtk+ GUI C Enum

30 Garrigue 29 (GADTs) type _ expr = Int : int -> int expr Add : (int -> int -> int) expr App : ( a -> b) expr * a expr -> b expr App (Add, Int 3) : (int -> int) expr

31 Garrigue 30 GADT let rec eval : type a. a expr -> a = function Int n -> n (* a = int *) Add -> (+) (* a = int -> int -> int *) App (f, x) -> eval f (eval x) (* *) val eval : a expr -> a = <fun> eval (App (App (Add, Int 3), Int 4));; - : int = 7

32 Garrigue 31 GADT type _ t = Int : int t let f (type a) (x : a t) = match x with Int -> 1 (* a = int *)

33 Garrigue 32 let f (type a) (x : a t) = match x with Int -> 1 (* a = int *) Haskell(GHC) OK OCaml

34 Garrigue 33 GADT exception Axiom type falso and p not = p -> falso let ex_falso (f : falso) = raise Axiom type ( a, b) ior = Inl of a Inr of b let classic () : ( a, a not) ior = raise Axiom (* Drinkers Paradox: x, Drinks(x ) y, Drinks(y) *) type _ drinks type all_drink = {all: y. unit -> y drinks} type non_drinker = Nd : x drinks not -> non_drinker type drinkers_paradox = Drinker : ( x drinks -> all_drink) -> drinkers_paradox let proof () : drinkers_paradox = match classic () with Inl (Nd nd) -> Drinker (fun d -> ex_falso (nd d)) Inr nnd -> Drinker (fun d -> {all = fun () -> match classic () with Inr nd -> ex_falso (nnd (Nd nd)) Inl d -> d})

35 Garrigue 34 let third l = match l with Cons (a, Cons (b, (Cons (c, l)))) -> c Cons (a, Cons (b, Nil)) -> b Nil -> raise Not_found Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Cons (_, Nil)

36 Garrigue 35 let f = function A -> 1 B -> 2 val f : [< A B ] -> int let g = function A -> 1 B -> 2 _ -> 3 val g : [> A B ] -> int let h = function A, A -> 1 A, B -> 2 B, _ -> 3 val h : [< A B ] * [< A B ] -> int

37 Garrigue 36 GADT GADT type _ t = Int : int t Bool : bool t let g : int t -> int = function Int -> 1 (* bool *) let h : type a. a t -> a t -> bool = fun x y -> match x, y with Int, Int -> true Bool, Bool -> true (* *)

38 Garrigue 37 GADT t let f : (char t) option -> int = function None -> 0 f char t int t bool t f t C i : ᾱ, ( β, τ i1... τ imi ) τ t GADT

39 Garrigue 38 OCaml

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

More Logic More Types ML/OCaml GADT Jacques Garrigue ( ) Jacques Le Normand (Google) Didier Rémy (INRIA) @garriguejej ocamlgadt ML Edinburgh LCF ML Curry-Howard ML ( ) ( ) ( ) ( ) 1 ( ) ML type nebou and