University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Disciplined‚ efficient‚ generalised folds for nested datatypes

Clare Martin‚ Jeremy Gibbons and Ian Bayley

Abstract

Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced generalised folds for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced efficient generalised folds to counter this inefficiency, but did so in a pragmatic way, at the cost of a loss of reasoning power: without categorical or equivalent underpinnings, there are no universal properties for manipulating folds. We combine the efficiency of Hinze's construction with the powerful reasoning tools of Bird and Paterson's.

Details

Journal

Formal Aspects of Computing

Number

1

Pages

19−35

Volume

16

Year

2004

Links

BibTeX

Link (pdf)

DOI (10.1007/s00165-003-0013-6)

Related pages

People

Activities