Iteration and coiteration schemes for higher-order and nested datatypes

Andreas Abel, Ralph Matthes, Tarmo Uustalu

Rannsóknarafurð: Framlag til fræðitímaritsRáðstefnugreinritrýni

42 Tilvitnanir (Scopus)

Útdráttur

This article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration and coiteration constructions to support as primitive. We propose and compare several well-behaved extensions of System Fω with some form of iteration and coiteration uniform in all kinds. In what we call Mendler-style systems, the iterator and coiterator have a computational behavior similar to the general recursor, but their types guarantee termination. In conventional-style systems, monotonicity witnesses are used for a notion of monotonicity defined uniformly for all kinds. Our most expressive systems GMItω and GItω of generalized Mendler, resp. conventional (co)iteration encompass Martin, Gibbons and Bailey's efficient folds for rank-2 inductive types. Strong normalization of all systems considered is proved by providing an embedding of the basic Mendler-style system MItω into System Fω.

Upprunalegt tungumálEnska
Síður (frá-til)3-66
Síðufjöldi64
FræðitímaritTheoretical Computer Science
Bindi333
Númer tölublaðs1-2
DOI
ÚtgáfustaðaÚtgefið - 1 mar. 2005
ViðburðurFoundations of Software Science and Computation Structures - Warsaw, Pólland
Tímalengd: 7 apr. 20039 apr. 2003

Fingerprint

Sökktu þér í rannsóknarefni „Iteration and coiteration schemes for higher-order and nested datatypes“. Saman myndar þetta einstakt fingrafar.

Vitna í þetta