Iteration and coiteration schemes for higher-order and nested datatypes

DOI10.1016/j.tcs.2004.10.017zbMath1070.68093OpenAlexW2105266034MaRDI QIDQ1770412

Tarmo Uustalu, Ralph Matthes, Andreas Abel

Publication date: 6 April 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.10.017

zbMATH Keywords

Strong normalizationIterationCoiterationEfficient foldsGeneralized foldsHigher-order datatypesHigher-order polymorphismSystem F\(^\omega\)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Related Items (18)

Classical Logic with Mendler Induction ⋮ A principled approach to programming with nested types in Haskell ⋮ Explicit substitutions and higher-order syntax ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Mixed Inductive/Coinductive Types and Strong Normalization ⋮ A realizability interpretation of Church's simple theory of types ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Fantastic morphisms and where to find them. A guide to recursion schemes ⋮ Unnamed Item ⋮ Polarised subtyping for sized types ⋮ Type-based termination of generic programs ⋮ Unnamed Item ⋮ Some Remarks on Type Systems for Course-of-value Recursion ⋮ An induction principle for nested datatypes in intensional type theory ⋮ From Coinductive Proofs to Exact Real Arithmetic ⋮ Modular Dependent Induction in Coq, Mendler-Style ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles ⋮ Heterogeneous Substitution Systems Revisited

Uses Software

• Haskell
• Polyp
• PolyLib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Polytypic values possess polykinded types
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• Type-indexed data types
• Disciplined, efficient, generalised folds for nested datatypes
• The Girard-Reynolds isomorphism
• Generalised folds for nested datatypes
• Inductive types and type constraints in the second-order lambda calculus
• Red-black trees with types
• Manufacturing datatypes
• Type classes with more higher-order polymorphism
• Faking it Simulating dependent types in Haskell
• de Bruijn notation as a nested datatype
• Generalizing generalized tries
• Red-black trees in a functional setting
• Monotone (co)inductive types and positive fixed-point types
• Generic Programming
• Generic Programming
• Generic Programming
• ML ^F
• Implementation of Functional Languages

This page was built for publication: Iteration and coiteration schemes for higher-order and nested datatypes