Polytypic Functions Over Nested Datatypes

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 theory is beautiful and well developed. It is a curse because the initial algebra semantics is restri...

Full description

Bibliographic Details
Main Author: Hinze, R
Format: Journal article
Published: 1999
_version_ 1826267576535089152
author Hinze, R
author_facet Hinze, R
author_sort Hinze, R
collection OXFORD
description 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 theory is beautiful and well developed. It is a curse because the initial algebra semantics is restricted to so-called regular datatypes. Recent work by R. Bird and L. Meertens on the semantics of non-regular or nested datatypes suggests that an extension to general datatypes is not entirely straightforward. Here we propose an alternative that extends polytypism to arbitrary datatypes, including nested datatypes and mutually recursive datatypes. The central idea is to use rational trees over a suitable set of functor symbols as type arguments for polytypic functions. Besides covering a wider range of types the approach is also simpler and technically less involving than previous ones. We present several examples of polytypic functions, among others polytypic reduction and polytypic equality. The presentation assumes some background in functional and in polytypic programming. A basic knowledge of monads is required for some of the examples.
first_indexed 2024-03-06T20:56:19Z
format Journal article
id oxford-uuid:3963b8d6-72d9-45ab-88dc-3530d11895d1
institution University of Oxford
last_indexed 2024-03-06T20:56:19Z
publishDate 1999
record_format dspace
spelling oxford-uuid:3963b8d6-72d9-45ab-88dc-3530d11895d12022-03-26T13:55:10ZPolytypic Functions Over Nested DatatypesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:3963b8d6-72d9-45ab-88dc-3530d11895d1Department of Computer Science1999Hinze, RThe 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 theory is beautiful and well developed. It is a curse because the initial algebra semantics is restricted to so-called regular datatypes. Recent work by R. Bird and L. Meertens on the semantics of non-regular or nested datatypes suggests that an extension to general datatypes is not entirely straightforward. Here we propose an alternative that extends polytypism to arbitrary datatypes, including nested datatypes and mutually recursive datatypes. The central idea is to use rational trees over a suitable set of functor symbols as type arguments for polytypic functions. Besides covering a wider range of types the approach is also simpler and technically less involving than previous ones. We present several examples of polytypic functions, among others polytypic reduction and polytypic equality. The presentation assumes some background in functional and in polytypic programming. A basic knowledge of monads is required for some of the examples.
spellingShingle Hinze, R
Polytypic Functions Over Nested Datatypes
title Polytypic Functions Over Nested Datatypes
title_full Polytypic Functions Over Nested Datatypes
title_fullStr Polytypic Functions Over Nested Datatypes
title_full_unstemmed Polytypic Functions Over Nested Datatypes
title_short Polytypic Functions Over Nested Datatypes
title_sort polytypic functions over nested datatypes
work_keys_str_mv AT hinzer polytypicfunctionsovernesteddatatypes