TWO EXTENSIONS OF SYSTEM FWITH (CO)ITERATION AND PRIMITIVE(CO)RECURSION PRINCIPLES

This paper presents two extensions of the second orderpolymorphic lambda calculus, system F, with monotone (co)inductivetypes supporting (co)iteration, primitive (co)recursion and inversionprinciples as primitives. One extension is inspired by the usual categoricalapproach to programming by means of initial algebras and finalcoalgebras; whereas the other models dialgebras, and can be seen as anextension of Hagino’s categorical lambda calculus within the frameworkof parametric polymorphism. The systems are presented in Curry-style,and are proven to be terminating and type-preserving. Moreover theirexpressiveness is shown by means of several programming examples,going from usual data types to lazy codata types such as streams orinfinite trees