Algebras and coalgebras in the light affine lambda calculus

Marco Gaboardi, Romain Péchoux

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Algebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. Interestingly, parametric polymorphism à la System F provides a way to encode algebras and coalgebras in strongly normalizing languages without losing the good logical properties of the calculus. Even if these encodings are sometimes unsatisfying because they provide only limited forms of algebras and coalgebras, they give insights on the expressivity of System F in terms of functions that we can program in it. With the goal of contributing to a better understanding of the expressivity of Implicit Computational Complexity systems, we study the problem of defining algebras and coalgebras in the Light Affine Lambda Calculus, a system characterizing the complexity class FPTIME. This system limits the computational complexity of programs but it also limits the ways we can use parametric polymorphism, and in general the way we can write our programs. We show here that while the restrictions imposed by the Light Affine Lambda Calculus pose some issues to the standard System F encodings, they still permit to encode some form of algebra and coalgebra. Using the algebra encoding one can define in the Light Affine Lambda Calculus the traditional inductive types. Unfortunately, the corresponding coalgebra encoding permits only a very limited form of coinductive data types. To extend this class we study an extension of the Light Affine Lambda Calculus by distributive laws for the modality §. This extension has been discussed but not studied before.

Original languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP
PublisherAssociation for Computing Machinery
Pages114-126
Number of pages13
Volume2015-August
ISBN (Print)9781450336697
DOIs
Publication statusPublished - 29 Aug 2015
Event20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015 - Vancouver, Canada
Duration: 31 Aug 20152 Sep 2015

Conference

Conference20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015
CountryCanada
CityVancouver
Period31/08/152/09/15

Keywords

  • Algebra and coalgebra
  • Implicit computational complexity
  • Light logics

Fingerprint Dive into the research topics of 'Algebras and coalgebras in the light affine lambda calculus'. Together they form a unique fingerprint.

Cite this