A principled approach to programming with nested types in Haskell

Patricia Johann, Neil Ghani

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.
LanguageEnglish
Pages155-189
Number of pages35
JournalHigher-Order and Symbolic Computation
Volume22
Issue number2
DOIs
Publication statusPublished - 30 Jun 2009

Fingerprint

Computer programming
Algebra
Semantics
Functional programming
Religious buildings
Computer programming languages
Fusion reactions

Keywords

  • initial algebras
  • nested types
  • short cut fusion
  • structured recursion
  • combinators
  • data type
  • functional programming languages
  • fusion rule
  • Haskell
  • modular programs
  • recursions

Cite this

@article{847d954f01d94cd9b42db7d2d3d43e38,
title = "A principled approach to programming with nested types in Haskell",
abstract = "Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.",
keywords = "initial algebras, nested types, short cut fusion, structured recursion, combinators, data type, functional programming languages, fusion rule, Haskell, modular programs, recursions",
author = "Patricia Johann and Neil Ghani",
year = "2009",
month = "6",
day = "30",
doi = "10.1007/s10990-009-9047-7",
language = "English",
volume = "22",
pages = "155--189",
journal = "Higher-Order and Symbolic Computation",
issn = "1388-3690",
number = "2",

}

A principled approach to programming with nested types in Haskell. / Johann, Patricia; Ghani, Neil.

In: Higher-Order and Symbolic Computation, Vol. 22, No. 2, 30.06.2009, p. 155-189.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A principled approach to programming with nested types in Haskell

AU - Johann, Patricia

AU - Ghani, Neil

PY - 2009/6/30

Y1 - 2009/6/30

N2 - Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.

AB - Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.

KW - initial algebras

KW - nested types

KW - short cut fusion

KW - structured recursion

KW - combinators

KW - data type

KW - functional programming languages

KW - fusion rule

KW - Haskell

KW - modular programs

KW - recursions

UR - http://link.springer.com/journal/10990

U2 - 10.1007/s10990-009-9047-7

DO - 10.1007/s10990-009-9047-7

M3 - Article

VL - 22

SP - 155

EP - 189

JO - Higher-Order and Symbolic Computation

T2 - Higher-Order and Symbolic Computation

JF - Higher-Order and Symbolic Computation

SN - 1388-3690

IS - 2

ER -