Two extensions of system F with (co)iteration and primitive (co)recursion principles
Departamento de Matemáticas, Facultad de Ciencias UNAM,
Circuito Exterior S/N. Ciudad Universitaria,
04510 México, D.F. México; firstname.lastname@example.org
Accepted: 16 July 2009
This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.
Mathematics Subject Classification: 03B40 / 68N18 / 68Q42 / 68Q65
Key words: Coiteration / corecursion / iteration / primitive recursion / system F / monotone inductive type / monotone coinductive type / monotonicity witness / saturated sets / algebras / coalgebras / dialgebras.
© EDP Sciences, 2009