# Bananas in space: extending fold and unfold to exponential types

@inproceedings{Meijer1995BananasIS, title={Bananas in space: extending fold and unfold to exponential types}, author={Erik Meijer and Graham Hutton}, booktitle={FPCA '95}, year={1995} }

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… Expand

#### Topics from this paper

#### 136 Citations

Polytypic Functions Over Nested Datatypes (Extended Abstract)

- Mathematics
- 1999

The theory and practice of polytypic programming is intimately connected with the initial algebra semantics of datatypes. This is both a blessing and a curse. It is a blessing because the underlying… Expand

Point-free program calculation

- Computer Science
- 2005

One of the contributions is a mechanism to translate classic pointwise code into the point-free style, which can be applied to a λ-calculus rich enough to represent the core functionality of a real functional programming language. Expand

Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism

- Computer Science
- ICFP '03
- 2003

This paper shows how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax, and derives "fusion laws" that functional programmers may use to reason about the iteration operator. Expand

Structured recursion for non-uniform data-types

- Computer Science
- 2000

This thesis shows how these recursion operators can be realized in the functional language Haskell, and presents a categorical semantics that supports formal reasoning about programs on non-uniform data-types. Expand

Down with variables

- Computer Science
- 2005

This paper presents a mechanism that allows programmers to convert classic point-wise code into point-free style, and a Haskell library that enables the direct execution of the resulting code. Expand

Polytypic Functions Over Nested Datatypes

- Computer Science, Mathematics
- Discret. Math. Theor. Comput. Sci.
- 1999

This work proposes an alternative that extends polytypism to arbitrary datatypes, including nesteddatatypes and mutually recursive datatype, and uses rational trees over a suitable set of functor symbols as type arguments for polytypic functions. Expand

Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism

- Computer Science
- J. Funct. Program.
- 2008

This paper shows how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax and derives “fusion laws” that functional programmers may use to reason about the iteration operator. Expand

Non-uniform Recursion: The solution (minimal sorting for fold)

- Mathematics
- 2000

A central data structure in functional programming languages like ML or Haskell are algebraic data types. I argue in this paper that the natural program structure to deal with algebraic data types is… Expand

Metamorphic Programming: Structured Recursion for Abstract Data Types

- Computer Science
- 1998

This work extends the structured recursive programming discipline, which favors the use of fold operations in place of general recursion, to abstract data types, and presents some laws for ADT folds and transformers and shows their use in program optimization and verification. Expand

Combining Datatypes and Effects

- Computer Science
- Advanced Functional Programming
- 2004

The way monads encapsulate effects plays an important role in the definition of the monadic recursion schemes, as it permits to focus on the structure of the recursive programs with effects disregarding the specific details of the effects involved. Expand

#### References

SHOWING 1-10 OF 51 REFERENCES

The category-theoretic solution of recursive domain equations

- Mathematics, Computer Science
- 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)
- 1977

The purpose of the present paper is to set up a categorical framework in which the known techniques for solving equations find a natural place, generalizing from least fixed-points of continuous functions over cpos to initial ones of continuous functors over $\omega $-categories. Expand

A system of constructor classes: overloading and implicit higher-order polymorphism

- Computer Science
- FPCA '93
- 1993

A flexible type system which combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes – a natural generalization of type classes in Haskell is described. Expand

A fold for all seasons

- Computer Science
- FPCA '93
- 1993

A normalization algorithm which automatically calculates improvements to programs expressed in a language based upon a generic promotion theorem rather than using an analysis phase to search for implicit structure, has important applications in program transformation, optimization, and theorem proving. Expand

Algebraic Approaches to Program Semantics

- Computer Science
- Texts and Monographs in Computer Science
- 1986

This book is an introduction to denotational semantics, introducing the reader to the order semantics of Scott and Strachey and the authors' own partially additive semantics. Expand

Relational properties of recursively defined domains

- Mathematics, Computer Science
- [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science
- 1993

A mixed induction/coinduction property of relations on recursively defined domains is described, working within a general framework for relations on domains and for actions of type constructors on… Expand

Recursive types reduced to inductive types

- Mathematics, Computer Science
- [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science
- 1990

It is shown that minimal invariant objects serve simultaneously as initial algebras and final coalgebra in the case that the bifunctor is independent of its contravariant variable and construable as a covariant functor. Expand

On the Relation between Direct and Continuation Semantics

- Computer Science
- ICALP
- 1974

This work gives two theorems which specify the relationship between the direct and the continuation semantic functions for a purely applicative language and shows that direct semantics are included in continuation semantics. Expand

Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire

- Computer Science
- FPCA
- 1991

A calculus for lazy functional programming based on recursion operators associated with data type definitions is developed and it is shown that all example functions in Bird and Wadler's Introduction to Functional Programming can be expressed using these operators. Expand

Programming Languages and Their Definition

- Computer Science
- Lecture Notes in Computer Science
- 1984

The semantics of parallel processing, nondeterministic functions and the semantics of CSP, and a model of nondeterminism: Indexed sets and their equivalence. Expand

Introduction to functional programming

- Computer Science
- Prentice Hall International series in computer science
- 1988

This is a thorough introduction to the fundamental concepts of functional programming that includes a simple, yet coherent treatment of the Haskell class; a calculus of time complexity; and new coverage of monadic input-output. Expand