Slide of the talk given by scm (http://www.iis.sinica.edu.tw/pages/scm/) on Functional Thursday Meet Up #12 (http://funth.kktix.cc/events/funth12).

Published on: **Mar 4, 2016**

Published in:
Science

Source: www.slideshare.net

- 1. Expressiveness and Model of the Polymorphic λ Calculus Shin-Cheng Mu IIS, Sinica Friday, April 11, 14
- 2. Motivation • V. Vene in APLAS 2004 [GUV04] gave a new proof of shortcut deforestation because it was only proved “informally by theorem-for free.” • But what’s wrong with theorem for free? • So I studied polymorphism and realised that there is a lot I did not know... Friday, April 11, 14
- 3. Parametricity, or the “theorems for free.” • Informally known by functional programmers as the “theorems for free.” • A polymorphic function’s type induces a “theorem”. • E.g. hd . map f = f . hd, for all hd:: [a]→a, regradless of its actual deﬁnition. • The word “theorem” may be mis-leading, however. [Wad89] Friday, April 11, 14
- 4. In this talk • Review some members of the λ calculus family: • Untyped λ calculus: λx . x • Simply-typed λ calculus: λx:Int . x • Polymorphic λ calculus: Λα.(λx:α . x), Δα.α--->τ, f [a] x • Consider their termination property, expressiveness, and model. Friday, April 11, 14
- 5. Untyped λ calculus • Not always terminating: (λx.(x x))(λx.(x x)) • Recursion: Y f = (λx . f (x x))(λx . f (x x)) • Equivalent to Turing machine (Church & Kleene). • Denotational model not trivial: requires Scott domains. Friday, April 11, 14
- 6. Simply-typed λ calculus • Strongly normalisable: all well-typed expression terminates. Y combinator cannot be typed. • Computes total functions only! • Has a simple model of total functions and sets. • Apparently cannot deﬁne some useful functions. But exactly how expressive? Friday, April 11, 14
- 7. The computability hierarchy partial recursive (functions) total recursive primitive recursive elementry recursive Friday, April 11, 14
- 8. Primitive recursion • A function that can be implemented using only for-loops (math world). It always terminate. • Zero: 0, succ: (1+), projection: (x1,...,xn)= xi. • Composition: f o g. • Primitive recursion: h(0,x) = f(x) h(n+1,x) = g (h(n),n,x) Friday, April 11, 14
- 9. Primitive recursion • A function that can be implemented using only for-loops (math world). It always terminate. • Zero: 0, succ: (1+), projection: (x1,...,xn)= xi. • Composition: f o g. • Primitive recursion: h(0,x) = f(x) h(n+1,x) = g (h(n),n,x) h(0) = c h(n+1) = g (h(n),n) Familiar? It’s paramorphism! [Mee90] Friday, April 11, 14
- 10. Partial and total recursion • Partial recursive functions: primitive recursion plus unbounded search: μf z = least x such that f(x,z) = 0. • The search may not terminate, thus introduces the partiality. • Partial rec. fn. is equiv. to Turing machine. • Total recursive functions: the subset of parital rec. fn. that is total. It’s bigger than primitive recursive functions! (eg. Ackermann’s function.) Friday, April 11, 14
- 11. Elementary recursion • Also called Kalmar elementary functions. Functions deﬁnable by 1, +, x, -., and SUM f (x,n) = Σn i=0 f(x,i) PRO f (x,n) = Πn i=0 f(x,i) • Deﬁnable functions include: mod, div, isPrime, etc. Friday, April 11, 14
- 12. Representing natural num. • Rep. of n over domain τ: λf:τ--->τ . λx:τ . f (... (f x)) with n occur. of f. • If we allow different instantiation of τ, we can deﬁne addition, multiplication, exp(Ii+1--> Ii---> Ii), predecessor(Ii+3---> Ii)... but not subtraction. • Therefore simply-typed calculus is weaker than elementary functions. Moreover, its value is bound by elementary fns. Friday, April 11, 14
- 13. • Use the type Δα.(α--->α)--->(α--->α) to represent natural numbers. • addition, multiplication, subtraction,pairs,.. • primrec = Δα.λg:N--->α--->α.λc:α. λn:N.snd(n[Nxα] (λz:Nxα.<1+fst z,g (fst z) (snd z)>) <0,c>) Polymorphism enhances expressiveness Friday, April 11, 14
- 14. • Use the type Δα.(α--->α)--->(α--->α) to represent natural numbers. • addition, multiplication, subtraction,pairs,.. • primrec = Δα.λg:N--->α--->α.λc:α. λn:N.snd(n[Nxα] (λz:Nxα.<1+fst z,g (fst z) (snd z)>) <0,c>) Polymorphism enhances expressiveness primrec = Δα.λg.λc. λn.snd (n (λz.<1+fst z,g (fst z) (snd z)>) <0,c>) Friday, April 11, 14
- 15. Ackermann’s function! Deﬁne ack without recursion? [Rey85] ack 0 n = n+1 ack (m+1) 0 = ack m 1 ack (m+1) (n+1) = ack m (ack (m+1) n) • Guess: ack = λm. m aug (1+) therefore ack (m+1) = aug (ack m) • ack (m+1) (n+1) = aug (ack m) (n+1) = ack m (aug (ack m) n) = ack m (ack (m+1) n) • We want aug f 0 = f 1 and aug f (n+1) = f (aug f n) • Solution: aug = λf. λn. (n+1) f 1 Friday, April 11, 14
- 16. Simulating data structures • Let list a = Δβ.(a--->β--->β) ---> β ---> β nil = Λβ.λf.λa.a cons x xs = Λβ.λf.λa. f x (xs f a) • append xs ys = xs cons ys • append = λxs:list a. λys:list a . xs[list a] (λx:a.λzs:list a . cons x zs) ys [Rey85] Friday, April 11, 14
- 17. Simulating data structures • Let list a = Δβ.(a--->β--->β) ---> β ---> β nil = Λβ.λf.λa.a cons x xs = Λβ.λf.λa. f x (xs f a) • append xs ys = xs cons ys • append = λxs:list a. λys:list a . xs[list a] (λx:a.λzs:list a . cons x zs) ys ! nil = Λβ.λf:a--->β--->β.λa:a.a cons x xs = Λβ.λf:a--->β--->β.λa:a. f x (xs f a) [Rey85] Friday, April 11, 14
- 18. Where does it stand? partial recursive (functions) total recursive primitive recursive elementry recursive Polymorphic λ Simply-typed λ Friday, April 11, 14
- 19. Fundamental sequence • Deﬁne f0(x) = x+1 • fn+1(x)= fx n(x) = fn(fn...(fn(x))..)... x applications. • f1(x)=2x, f2(x)=2x ×x • fΘ(x)=fΘ[x](x) for limit ordinal Θ. • Limit ordinals: ω is the size of natural numbers, ε0 is the limit of ω, ωω , ωωω ..... Friday, April 11, 14
- 20. Hierarchy characterised by rate of growth • Running time of elementary functions are bounded by fn 2(x) for some n. • Time of primitive recursive functions are bounded by fn(x) for some n< ω. • Ackermann’s function is essentially fω(x). • fε0(x) is representable in polymorphic λ calculus! • It represents exactly the functions provably recursive in 2nd-order arithmetic -- a much larger class than fε0(x). [FLD83] Friday, April 11, 14
- 21. Termination • Still, every function deﬁned in poly-λ terminates. • However, the termination cannot be proved in Peano arithmetic! • Peano arithmetic: 0, (1+), addition, induction... covering most techniques we use in proofs of programs. • Godel’s incompleteness theorem stated that there are true theorems not provable in PA. This was the ﬁrst “interesting” example. [FLD83] Friday, April 11, 14
- 22. Model for poly. λ calculus? • Untyped λ: not terminating, needs domain. • Simple-typed λ: terminating, set-theoretic. • λx:Int.x is the id for Int, λx:Char.x for Char. • Poly. λ: can we avoid using domains? • First try: a polymorphic function is a collection of functions indexed by type. • Λα.λx:α.x is a collection of identity fns. • However, that would include some ad-hoc functions. Friday, April 11, 14
- 23. Parametricity • Reynolds restricts polymorphic objects to parametric values: • Let p: Δα.τ. It is parametric if for all set assignments s1, s2, and r s1×s2: 〈p s1, p s2〉 [id|α:r]# τ • Which later became “theorem for free”. • Reynolds [Rey83] believed that there is a set- theoretic model for poly. λ where poly. objects represent parametric values. • He then falsiﬁed his conjecture [Rey84]. [Wad89] Friday, April 11, 14
- 24. No simple model! • Bool can be represented by B=Δα.α--->α--->α • Let Ts = (s--->B)--->B for all type s, and Tf = λh.λg.h(g o f) (for all f: s--->t, Tf: Ts--->Tt). • Let P=(((s--->B)--->B)--->s)--->s. We can construct a h: TP--->P s.t. the diagram commutes for all f. • In fact h is an initial algebra! • But that would make TP isomorphic to P, which is a contradiction (they have diff. cardinalities unless |B|=1). h P TP s Ts Tgg f [Rey84]Polymor phism is not set-theoretic. f. g. Friday, April 11, 14
- 25. Later models • Using topos [Pit87]Poly. is set-theoretic, constructively. • Frame [BM84][MM85][Wad89]. • Functorial approach [BFS90]. • Operational aspects [Pit00]. • Used to prove short-cut fusion [Joh03]. Friday, April 11, 14
- 26. What’s the use of parametricity? • It’s still a key concept! Recall representation of lists: llist a = Δβ.(a--->β--->β) ---> β ---> β. • In general, the least ﬁxed-point of functor F (or the inital F-algebra) can be represented by Δβ.(F β--->β) ---> β... iff parametricity holds! • Types deﬁned as least-ﬁxed-points are called inductive. • nil = Λβ.λf.λa.a, cons x xs = Λβ.λf.λa. f x (xs f a), x = cons 1 (cons 2 (cons 3 nil). [Has94] Friday, April 11, 14
- 27. Inductive and coinductive datatypes • The greatest ﬁxed-point of functor F can be represented by ∃x.(x → F x, x), iff parametricity holds. It’s called coinductive. • from n = (λm.Right (m,m+1), n) :: glist a • When least and greatest ﬁxed-points coincide (i.e. exists a force:: glist a →llist a), we can do hylomorphism. [Has94] [How96] Friday, April 11, 14
- 28. Pointed types • In a model where parametricity and extensionality holds, the following are equivalent: • Inductive and coinductive types coincide; • Exists a ﬁxed-point operator for values; • Exists a ﬁxed-point operator for types. [Has94] ? Friday, April 11, 14
- 29. Conclusion Termination Expressiveness Model Untyped NO = Turing machine domain Simply typed YES < elementry fn. set & functio n Polymorphic YES but not provable in PA > Ackermann domain or non-trivial sets Friday, April 11, 14
- 30. What I learnt from this history study... • Adding polymorphism to a language strongly enhances its power. • The concept of fold, etc., ﬁnds its root in very fundamental research. • Category theory has played an important role in early stage of computing science. • Parametricity is an important assumption leading to many useful properties. Friday, April 11, 14
- 31. References • [FLD83] S.Fortune, D. Leivant, M. O’Donnell, The expressiveness of simple and second-order type structures. In Journal of the ACM, 30(1), pp 151-185. • [Rey83] J.C. Reynolds. Types, abstractions and parametric polymorphism. In Information Processing 83, pp 513-523. • [BM84]K.B. Bruce, A.R. Meyer, The semantics of second-order polymorphic lambda calculus. In Semantics of Data Types, LNCS 173. • [Rey84] J.C. Reynolds, Polymorphism is not set theoretic. In Semantics of data Types, LNCS 173, pp 145-156. • [MM85] J.C. Mitchell, A.R. Meyer, Second-order logical relations. In Logics of Programs, LNCS 193. • [Rey85] J.C. Reynolds, Three approaches to type structure. In Mathematical Foundations of Software Development, LNCS 185. Friday, April 11, 14
- 32. References • [Pit87] A.M. Pitts, Polymorphism is set theoretic, constructively. In Category Theory and Computer Science, LNCS 283, pp 12-39. • [Wad89] P. Wadler, Theorems for free! In Int. Sym. on Functional Programming Languages and Computer Architecture, ‘89. • [BFS90] E.S. Bainbridge, P.J. Freyd, A. Scedrov, P.J. Scott, Functorial polymorphism. In Theoretical computer science v.70, pp 36-54. • [Mee90] L. Meertens, Paramorphisms. In Formal Aspects of Computing. • [Has94] R. Hasegawa. Categorical data types in parametric polymorphism. Math. Structures in Computer Science, March 1994. • [How96] B.T. Howard. Inductive, coinductive, and pointed types. ICFP 96. • [Pit00] A.M. Pitts, Parametric polymorphism and operational equivalence. In Math. Struct. in Comp. Science v.10, pp 1-39. • [Joh03] P. Johann, Short cut fusion is correct. In J. Functional Programming v.13, pp 797-814. • [GUV04]N. Ghani, T. Uustalu, V, Vene, Build, augment and destory. In APLAS 2004, LNCS 3002, pp 327-347. Friday, April 11, 14