Coq with Classes. Matthieu Sozeau. JFLA 2012 February 4th-7th 2012 Carnac, France. Project Team πr 2 INRIA Paris & PPS, Paris 7 University - PDF

Description
Coq with Classes Matthieu Sozeau Project Team πr 2 INRIA Paris & PPS, Paris 7 University JFLA 2012 February 4th-7th 2012 Carnac, France Outline 1 Type Classes theory: from Haskell to Coq 2 Demonstrations

Please download to get full document.

View again

of 97
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Food & Beverages

Publish on:

Views: 40 | Pages: 97

Extension: PDF | Download: 0

Share
Transcript
Coq with Classes Matthieu Sozeau Project Team πr 2 INRIA Paris & PPS, Paris 7 University JFLA 2012 February 4th-7th 2012 Carnac, France Outline 1 Type Classes theory: from Haskell to Coq 2 Demonstrations Matthieu Sozeau - Coq with Classes 2 Type Classes 1 Type Classes in theory Motivation and setup Type Classes from Haskell Type Classes in Coq 2 Type Classes in practice Playing with numbers Instance Inference Dependent Classes A programming example: Generic exponentiation A structuring tool: Building hierarchies Logic programming: Reification 3 Summary Related and future work Matthieu Sozeau - Coq with Classes 3 Goal Enhancing type inference through overloading: For generic programming with interfaces rather than concrete implementations. Akin to a first-class module system. For generic proof scripts: refer to proofs by semantic concept rather than name. E.g. reflexivity of R instead of R refl. In general, allows inference of arbitrary additional structure on a given type or value. Matthieu Sozeau - Coq with Classes 4 Solutions for overloading Context: Modularity: separate definitions of the specializations. Constrained by Coq: a fixed kernel language! Matthieu Sozeau - Coq with Classes 5 Solutions for overloading Context: Modularity: separate definitions of the specializations. Constrained by Coq: a fixed kernel language! Existing paradigms: Intersection types: closed overloading by declaring multiple signatures for a single constant (e.g. CDuce, Stardust). Bounded quantification and class-based overloading. Overloading circumscribed by a subtyping relation (e.g. structural subtyping à la OCaml). Matthieu Sozeau - Coq with Classes 5 Solutions for overloading Context: Modularity: separate definitions of the specializations. Constrained by Coq: a fixed kernel language! Existing paradigms: Intersection types: closed overloading by declaring multiple signatures for a single constant (e.g. CDuce, Stardust). Bounded quantification and class-based overloading. Overloading circumscribed by a subtyping relation (e.g. structural subtyping à la OCaml). Solution: Elaborate Type Classes, a kind of bounded quantification where the subtyping relation needs not be internalized. Matthieu Sozeau - Coq with Classes 5 Making ad-hoc polymorphism less ad hoc In Haskell, Wadler & Blott, POPL 89. Also in Isabelle, Nipkow & Snelting, FPCA 91. class Eq a where (==) :: a a Bool Matthieu Sozeau - Coq with Classes 6 Making ad-hoc polymorphism less ad hoc In Haskell, Wadler & Blott, POPL 89. Also in Isabelle, Nipkow & Snelting, FPCA 91. class Eq a where (==) :: a a Bool instance Eq Bool where x == y = if x then y else not y Matthieu Sozeau - Coq with Classes 6 Making ad-hoc polymorphism less ad hoc In Haskell, Wadler & Blott, POPL 89. Also in Isabelle, Nipkow & Snelting, FPCA 91. class Eq a where (==) :: a a Bool instance Eq Bool where x == y = if x then y else not y in :: Eq a a [a] Bool in x [] = False in x (y : ys) = x == y in x ys Matthieu Sozeau - Coq with Classes 6 Parametrized instances and super-classes instance (Eq a) Eq [a] where [] == [] = True (x : xs) == (y : ys) = x == y && xs == ys == = False Matthieu Sozeau - Coq with Classes 7 Parametrized instances and super-classes instance (Eq a) Eq [a] where [] == [] = True (x : xs) == (y : ys) = x == y && xs == ys == = False class Num a where (+) :: a a a... class (Num a) Fractional a where (/) :: a a a... Matthieu Sozeau - Coq with Classes 7 Type Classes 1 Type Classes in theory Motivation and setup Type Classes from Haskell Type Classes in Coq 2 Type Classes in practice Playing with numbers Instance Inference Dependent Classes A programming example: Generic exponentiation A structuring tool: Building hierarchies Logic programming: Reification 3 Summary Related and future work Matthieu Sozeau - Coq with Classes 8 Extension to Coq Overloading of names in programs, specifications and proofs. Matthieu Sozeau - Coq with Classes 9 Extension to Coq Overloading of names in programs, specifications and proofs. A safer Haskell Proofs are part of instances. Class Eq A := { eqb : A A bool ; eq eqb : x y : A, x = y eqb x y = true }. Matthieu Sozeau - Coq with Classes 9 Extension to Coq Overloading of names in programs, specifications and proofs. A safer Haskell Proofs are part of instances. Class Eq A := { eqb : A A bool ; eq eqb : x y : A, x = y eqb x y = true }. Types and values are unified Dependent types give new power to type classes. Class Reflexive A (R : relation A) := reflexive : x, R x x. Matthieu Sozeau - Coq with Classes 9 A cheap implementation Parametrized dependent records Class Id (α 1 : τ 1 ) (α n : τ n ) := {f 1 : φ 1 ; ; f m : φ m }. Matthieu Sozeau - Coq with Classes 10 A cheap implementation Parametrized dependent records Record Id (α 1 : τ 1 ) (α n : τ n ) := {f 1 : φ 1 ; ; f m : φ m }. Matthieu Sozeau - Coq with Classes 10 A cheap implementation Parametrized dependent records Record Id (α 1 : τ 1 ) (α n : τ n ) := {f 1 : φ 1 ; ; f m : φ m }. Instances are just definitions of type Id t n. Matthieu Sozeau - Coq with Classes 10 A cheap implementation Parametrized dependent records Record Id (α 1 : τ 1 ) (α n : τ n ) := {f 1 : φ 1 ; ; f m : φ m }. Instances are just definitions of type Id t n. Custom implicit arguments of projections f 1 : α n : τ n, Id α n φ 1 Matthieu Sozeau - Coq with Classes 10 A cheap implementation Parametrized dependent records Record Id (α 1 : τ 1 ) (α n : τ n ) := {f 1 : φ 1 ; ; f m : φ m }. Instances are just definitions of type Id t n. Custom implicit arguments of projections f 1 : { α n : τ n }, {Id α n } φ 1 Matthieu Sozeau - Coq with Classes 10 Elaboration with classes, an example (λx y : bool. eqb x y) Matthieu Sozeau - Coq with Classes 11 Elaboration with classes, an example (λx y : bool. eqb x y) { Implicit arguments } (λx y : (? A : Type) (? eq : Eq? A ) x y) Matthieu Sozeau - Coq with Classes 11 Elaboration with classes, an example (λx y : bool. eqb x y) { Implicit arguments } (λx y : (? A : Type) (? eq : Eq? A ) x y) { Unification } (λx y : bool (? eq : Eq bool) x y) Matthieu Sozeau - Coq with Classes 11 Elaboration with classes, an example (λx y : bool. eqb x y) { Implicit arguments } (λx y : (? A : Type) (? eq : Eq? A ) x y) { Unification } (λx y : bool (? eq : Eq bool) x y) { Proof search for Eq bool returns Eq bool } (λx y : bool Eq bool x y) Matthieu Sozeau - Coq with Classes 11 Type Class resolution Proof-search tactic with instances as lemmas: A : Type, eqa : Eq A? : Eq (list A) Simple depth-first search with higher-order unification Returns the first solution only + Extensible through Ltac Matthieu Sozeau - Coq with Classes 12 Type Classes 1 Type Classes in theory Motivation and setup Type Classes from Haskell Type Classes in Coq 2 Type Classes in practice Playing with numbers Instance Inference Dependent Classes A programming example: Generic exponentiation A structuring tool: Building hierarchies Logic programming: Reification 3 Summary Related and future work Matthieu Sozeau - Coq with Classes 13 Numeric overloading Class Num α := { zero : α ; one : α ; plus : α α α }. Matthieu Sozeau - Coq with Classes 14 Numeric overloading Class Num α := { zero : α ; one : α ; plus : α α α }. Instance nat num : Num nat := { zero := 0%nat ; one := 1%nat ; plus := Peano.plus }. Instance Z num : Num Z := { zero := 0%Z ; one := 1%Z ; plus := Zplus }. Matthieu Sozeau - Coq with Classes 14 Numeric overloading Class Num α := { zero : α ; one : α ; plus : α α α }. Instance nat num : Num nat := { zero := 0%nat ; one := 1%nat ; plus := Peano.plus }. Instance Z num : Num Z := { zero := 0%Z ; one := 1%Z ; plus := Zplus }. Notation 0 := zero. Notation 1 := one. Infix + := plus. Matthieu Sozeau - Coq with Classes 14 Numeric overloading Class Num α := { zero : α ; one : α ; plus : α α α }. Instance nat num : Num nat := { zero := 0%nat ; one := 1%nat ; plus := Peano.plus }. Instance Z num : Num Z := { zero := 0%Z ; one := 1%Z ; plus := Zplus }. Notation 0 := zero. Notation 1 := one. Infix + := plus. Check (λ x : nat, x + ( x)). Check (λ x : Z, x + ( x)). Matthieu Sozeau - Coq with Classes 14 Numeric overloading Class Num α := { zero : α ; one : α ; plus : α α α }. Instance nat num : Num nat := { zero := 0%nat ; one := 1%nat ; plus := Peano.plus }. Instance Z num : Num Z := { zero := 0%Z ; one := 1%Z ; plus := Zplus }. Notation 0 := zero. Notation 1 := one. Infix + := plus. Check (λ x : nat, x + ( x)). Check (λ x : Z, x + ( x)). Defaulting Check (λ x, x + 1). Matthieu Sozeau - Coq with Classes 14 Instance inference Class EqDec A := { eq dec : x y : A, {x = y} + {x y} }. Instance: EqDec nat := { eq dec := eq nat dec }. Instance: EqDec bool := { eq dec := bool dec }. Matthieu Sozeau - Coq with Classes 15 Instance inference Class EqDec A := { eq dec : x y : A, {x = y} + {x y} }. Instance: EqDec nat := { eq dec := eq nat dec }. Instance: EqDec bool := { eq dec := bool dec }. Program Instance: A, EqDec A EqDec (option A) := { eq dec x y := match x, y with None, None in left Some x, Some y if eq dec x y then in left else in right, in right end }. Check (λ x : option (option nat), eq dec x None). : x : option (option nat), {x = None} + {x None} Matthieu Sozeau - Coq with Classes 15 Dependent classes Class Reflexive {A} (R : relation A) := refl : x, R x x. Matthieu Sozeau - Coq with Classes 16 Dependent classes Class Reflexive {A} (R : relation A) := refl : x, R x x. Instance eq refl A : Reflexive A) equal A. Instance iff refl : Reflexive iff. Proof. red. tauto. Qed. Matthieu Sozeau - Coq with Classes 16 Dependent classes Class Reflexive {A} (R : relation A) := refl : x, R x x. Instance eq refl A : Reflexive A) equal A. Instance iff refl : Reflexive iff. Proof. red. tauto. Qed. Goal P, P P. Proof. apply refl. Qed. Goal A (x : A), x = x. Proof. intros A ; apply refl. Qed. Matthieu Sozeau - Coq with Classes 16 Dependent classes Class Reflexive {A} (R : relation A) := refl : x, R x x. Instance eq refl A : Reflexive A) equal A. Instance iff refl : Reflexive iff. Proof. red. tauto. Qed. Goal P, P P. Proof. apply refl. Qed. Goal A (x : A), x = x. Proof. intros A ; apply refl. Qed. Ltac refl := apply refl. Lemma foo {Reflexive nat R} : R 0 0. Proof. intros. refl. Qed. Matthieu Sozeau - Coq with Classes 16 Type Classes 1 Type Classes in theory Motivation and setup Type Classes from Haskell Type Classes in Coq 2 Type Classes in practice Playing with numbers Instance Inference Dependent Classes A programming example: Generic exponentiation A structuring tool: Building hierarchies Logic programming: Reification 3 Summary Related and future work Matthieu Sozeau - Coq with Classes 17 Implicit Generalization An old convention: the free variables of a statement are implicitly universally quantified. E.g., when defining a set of equations: x + y = y + x x + 0 = 0 x + S y = S (x + y) Matthieu Sozeau - Coq with Classes 18 Implicit Generalization An old convention: the free variables of a statement are implicitly universally quantified. E.g., when defining a set of equations: x + y = y + x x + 0 = 0 x + S y = S (x + y) We introduce new syntax to automatically generalize the free variables of a given term or binder, as implicit arguments: Γ : (t) : Type Γ : Π FV(t)\Γ, t Γ : (t) : T : Type Γ : λ FV(t)\Γ, t (x i : τ i ) {y : T } (x i : τ i ) {FV(T ) \ x i } {y : T } (x i : τ i ) (y : T ) (x i : τ i ) {FV(T ) \ x i } (y : T ) Matthieu Sozeau - Coq with Classes 18 Monomorphic binary power The following definition is very naïve, but obviously correct: Fixpoint power (a : Z) (n : nat) := match n with 0%nat 1 S p a power a p end. Eval vm compute in power = : Z Matthieu Sozeau - Coq with Classes 19 An efficient tail-recursive version This one is more efficient but relies on a more elaborate property: Function binary power mult (acc x : Z) (n : nat) {measure (fun i i) n} : Z := match n with 0%nat acc if Even.even odd dec n then binary power mult acc (x x) (div2 n) else binary power mult (acc x) (x x) (div2 n) end. Definition binary power (x:z) (n:nat) := binary power mult 1 x n. Eval vm compute in binary power = : Z Goal binary power = power Proof. reflexivity. Qed. Matthieu Sozeau - Coq with Classes 20 Questions Is binary power correct (w.r.t. power)? Matthieu Sozeau - Coq with Classes 21 Questions Is binary power correct (w.r.t. power)? Is it worth proving this correctness only for powers of integers? Matthieu Sozeau - Coq with Classes 21 Questions Is binary power correct (w.r.t. power)? Is it worth proving this correctness only for powers of integers? And prove it again for powers of real numbers, matrices? Matthieu Sozeau - Coq with Classes 21 Questions Is binary power correct (w.r.t. power)? Is it worth proving this correctness only for powers of integers? And prove it again for powers of real numbers, matrices? NO! We aim to prove the equivalence between power and binary power for any structure consisting of a binary associative operation that admits a neutral element, i.e. any monoid. Matthieu Sozeau - Coq with Classes 21 Monoids Class Monoid {A:Type} (dot : A A A) (one : A) : Type := { dot assoc : x y z : A, dot x (dot y z) = dot (dot x y) z; one left : x, dot one x = x; one right : x, dot x one = x }. Operations as parameters to ease sharing, allows to specify multiple monoids on the same carrier unambiguously, e.g. Monoid 0 plus and Monoid 1 mult. Matthieu Sozeau - Coq with Classes 22 Implicit Generalization Quantification becomes verbose: Definition two {A dot one} {M A dot one} := dot one one. Using implicit generalization: Generalizable Variables A dot one. Definition three {Monoid A dot one} := dot two one. Matthieu Sozeau - Coq with Classes 23 Generic notations One can define trivial projections to recover global names for parameters: Definition monop {Monoid A dot one} := dot. Definition monunit {Monoid A dot one} := one. and the corresponding generic notations: Infix := monop. Notation 1 := monunit. Matthieu Sozeau - Coq with Classes 24 Generic power Let s redefine power and binary power generically. Section Power. Context {Monoid A dot one}. All following definitions are overloaded over any Monoid structure. Fixpoint power (a : A) (n : nat) := match n with 0%nat 1 S p a (power a p) end. Lemma power of unit : n : nat, power 1 n = 1. Proof.... Qed. Matthieu Sozeau - Coq with Classes 25 Generic binary exponentiation Function binary power mult (acc x : A) (n : nat) {measure (fun i i) n} : A := match n with 0%nat acc if Even.even odd dec n then binary power mult acc (x x) (div2 n) else binary power mult (acc x) (x x) (div2 n) end. Definition binary power (x : A) (n : nat) := binary power mult 1 x n. Lemma binary spec x n : power x n = binary power x n. Proof.... Qed. End Power. Matthieu Sozeau - Coq with Classes 26 Instantiation Let s build a Monoid instance. Instance ZMult : Monoid Zmult 1%Z. Proof. split. subgoal 1 is: x y z : Z, x (y z) = x y z subgoal 2 is: x : Z, 1 x = x subgoal 3 is: x : Z, x 1 = x... Qed. Matthieu Sozeau - Coq with Classes 27 Instantiation We can now use the overloaded power on our new Monoid. About power. : (A : Type) (dot : A A A) (one : A), Monoid dot one A nat A Arguments A, dot, one, H are implicit and maximally inserted Matthieu Sozeau - Coq with Classes 28 Instantiation We can now use the overloaded power on our new Monoid. About power. : (A : Type) (dot : A A A) (one : A), Monoid dot one A nat A Arguments A, dot, one, H are implicit and maximally inserted Set Printing Implicit. Check power 2 Z Z.mul 1 ZMult : Z Matthieu Sozeau - Coq with Classes 28 Instantiation We can now use the overloaded power on our new Monoid. About power. : (A : Type) (dot : A A A) (one : A), Monoid dot one A nat A Arguments A, dot, one, H are implicit and maximally inserted Set Printing Implicit. Check power 2 Z Z.mul 1 ZMult : Z Compute power = : Z Matthieu Sozeau - Coq with Classes 28 The monoid of square matrices Live demo Matthieu Sozeau - Coq with Classes 29 Type Classes 1 Type Classes in theory Motivation and setup Type Classes from Haskell Type Classes in Coq 2 Type Classes in practice Playing with numbers Instance Inference Dependent Classes A programming example: Generic exponentiation A structuring tool: Building hierarchies Logic programming: Reification 3 Summary Related and future work Matthieu Sozeau - Coq with Classes 30 Building hierarchies of classes: superclasses Superclasses become parameters: Class (Num α) Frac α := { div : α { y : α y 0 } α }. Class Frac α {Num α} := { div : α { y : α y 0 } α }. Matthieu Sozeau - Coq with Classes 31 Building hierarchies of classes: superclasses Superclasses become parameters: Class (Num α) Frac α := { div : α { y : α y 0 } α }. Class Frac α {Num α} := { div : α { y : α y 0 } α }. + Support for binding super-classes by implicit generalization: Program Definition div2 {Frac α} (a : α) := div a (1 + 1). Definition div2 {α} {N : Num α} {Frac α N} (a : α) :=... Matthieu Sozeau - Coq with Classes 31 Building hierarchies of classes: subinstances Substructures become subinstances: Class Monoid A := { monop : A A A ;... } Class Group A := { grp mon : Monoid A ;... } Matthieu Sozeau - Coq with Classes 32 Building hierarchies of classes: subinstances Substructures become subinstances: Class Monoid A := { monop : A A A ;... } Class Group A := { grp mon : Monoid A ;... } Instance grp mon {Group A} : Monoid A. Matthieu Sozeau - Coq with Classes 32 Building hierarchies of classes: subinstances Substructures become subinstances: Class Monoid A := { monop : A A A ;... } Class Group A := { grp mon : Monoid A ;... } Instance grp mon {Group A} : Monoid A. Definition foo {Group A} (x : A) : A := monop x x. Similar to the existing Structures based on coercive subtyping. Matthieu Sozeau - Coq with Classes 32 Fields or Parameters? When one doesn t have manifest types and with constraints... Class Functor := { A : Type; B : Type; src : Category A ; dst : Category B ;... } or Class Functor A B := { src : Category A; dst : Category B;... } or Class Functor A (src : Category A) B (dst : Category B) :=...??? Matthieu Sozeau - Coq with Classes 33 Sharing by equalities Definition adjunction (F : Functor) (G : Functor), src F = dst G dst F = src G... Obfuscates the goals and the computations, awkward to use. Matthieu Sozeau - Coq with Classes 34 Sharing by parameters Class (C : Category obj, D : Category obj ) Functor :=... Class Functor (C : Category obj, D : Category obj ) :=... Matthieu Sozeau - Coq with Classes 35 Sharing by parameters Class (C : Category obj, D : Category obj ) Functor :=... Class Functor (C : Category obj, D : Category obj ) :=... Record Functor {obj} (C : Category obj) {obj }(D : Category obj ) :=... Matthieu Sozeau - Coq with Classes 35 Sharing by parameters Class (C : Category obj, D : Category obj ) Functor :=... Class Functor (C : Category obj, D : Category obj ) :=... Record Functor {obj} (C : Category obj) {obj }(D : Category obj ) :=... Definition adjunction {C : Category obj, D : Category obj } (F : Functor C D) (G : Functor D C) :=... Uses the dependent product and named, first-class instances. Matthieu Sozeau - Coq with Classes 35 Category Class Category (obj : Type) (hom : obj obj Type) := { morphisms : a b, Setoid (hom a b) ; id : {a}, hom a a; compose : {a b c}, hom a b hom b c hom a c where x y := (compose y x); id unit left : (f : hom a b), f id == f ; id unit right : (f : hom a b), id f == f ; assoc : a b c d (f : hom a b) (g : hom b c) (h : hom c d), h (g f ) == (h g) f }. Matthieu Sozeau - Coq with Classes 36 Abstract instances Definition opposite (X : Type) := X. Program Instance opposite category ( Category obj hom ) : Category (opposite obj) (flip hom). Matthieu Sozeau - Coq with Classes 37 Abstract instances Definition opposite (X : Type) := X. Program Instance opposite category ( Category obj hom ) : Category (opposite obj) (flip hom). Class Terminal (C : Category obj hom) (one : obj)
Related Search
Similar documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks