Bananas in space: extending fold and unfold to exponential types

Fold and unfold are general purpose functionals for process-ing and constructing lists. By using the categorical approach of modelling recursive datatypes as fixed points of functors, these functionals and their algebraic properties were generalised from lists to polynomial (sum-of-product) datatype...

Full description

Bibliographic Details
Main Authors: Meijer, Erik, Hutton, Graham
Format: Conference or Workshop Item
Published: ACM Press, La Jolla, California 1995
Online Access:https://eprints.nottingham.ac.uk/28198/
_version_ 1848793522989170688
author Meijer, Erik
Hutton, Graham
author_facet Meijer, Erik
Hutton, Graham
author_sort Meijer, Erik
building Nottingham Research Data Repository
collection Online Access
description Fold and unfold are general purpose functionals for process-ing and constructing lists. By using the categorical approach of modelling recursive datatypes as fixed points of functors, these functionals and their algebraic properties were generalised from lists to polynomial (sum-of-product) datatypes. However, the restriction to polynomial datatypes is a serious limitation: it precludes the use of exponentials (function-spaces), whereas it is central to functional programming that functions are first-class values, and so exponentials should be able to be used freely in datatype definitions. In this paper we explain how Freyd’s work on modelling recursive datatypes as fixed points of difunctors shows how to generalise fold and unfold from polynomial datatypes to those involving exponentials. Knowledge of category theory is not required; we use Gofer throughout as our meta-language, making extensive use of constructor classes
first_indexed 2025-11-14T19:01:39Z
format Conference or Workshop Item
id nottingham-28198
institution University of Nottingham Malaysia Campus
institution_category Local University
last_indexed 2025-11-14T19:01:39Z
publishDate 1995
publisher ACM Press, La Jolla, California
recordtype eprints
repository_type Digital Repository
spelling nottingham-281982020-05-04T20:33:32Z https://eprints.nottingham.ac.uk/28198/ Bananas in space: extending fold and unfold to exponential types Meijer, Erik Hutton, Graham Fold and unfold are general purpose functionals for process-ing and constructing lists. By using the categorical approach of modelling recursive datatypes as fixed points of functors, these functionals and their algebraic properties were generalised from lists to polynomial (sum-of-product) datatypes. However, the restriction to polynomial datatypes is a serious limitation: it precludes the use of exponentials (function-spaces), whereas it is central to functional programming that functions are first-class values, and so exponentials should be able to be used freely in datatype definitions. In this paper we explain how Freyd’s work on modelling recursive datatypes as fixed points of difunctors shows how to generalise fold and unfold from polynomial datatypes to those involving exponentials. Knowledge of category theory is not required; we use Gofer throughout as our meta-language, making extensive use of constructor classes ACM Press, La Jolla, California 1995-06 Conference or Workshop Item PeerReviewed Meijer, Erik and Hutton, Graham (1995) Bananas in space: extending fold and unfold to exponential types. In: International Conference on Functional Programming Languages and Computer Architecture (7th), 26-28 June 1995, La Jolla, California, USA. http://dl.acm.org/citation.cfm?doid=224164.224225
spellingShingle Meijer, Erik
Hutton, Graham
Bananas in space: extending fold and unfold to exponential types
title Bananas in space: extending fold and unfold to exponential types
title_full Bananas in space: extending fold and unfold to exponential types
title_fullStr Bananas in space: extending fold and unfold to exponential types
title_full_unstemmed Bananas in space: extending fold and unfold to exponential types
title_short Bananas in space: extending fold and unfold to exponential types
title_sort bananas in space: extending fold and unfold to exponential types
url https://eprints.nottingham.ac.uk/28198/
https://eprints.nottingham.ac.uk/28198/