### Abstract

Original language | English |
---|---|

Title of host publication | Algebra and Coalgebra in Computer Science |

Subtitle of host publication | 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings |

Editors | Reiko Heckel, Stefan Milius |

Place of Publication | Berlin |

Pages | 19-33 |

Number of pages | 15 |

DOIs | |

Publication status | Published - 8 Aug 2013 |

Event | 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 - Warsaw, Poland Duration: 3 Sep 2013 → 6 Sep 2013 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 8089 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 |
---|---|

Country | Poland |

City | Warsaw |

Period | 3/09/13 → 6/09/13 |

### Fingerprint

### Keywords

- data type
- generalisation
- inductive-recursive definitions
- initial algebras
- natural transformations
- nested data
- new theory
- set-theoretic models

### Cite this

*Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings*(pp. 19-33). (Lecture Notes in Computer Science; Vol. 8089). Berlin. https://doi.org/10.1007/978-3-642-40206-7_3

}

*Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings.*Lecture Notes in Computer Science, vol. 8089, Berlin, pp. 19-33, 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Warsaw, Poland, 3/09/13. https://doi.org/10.1007/978-3-642-40206-7_3

**Positive inductive-recursive definitions.** / Ghani, Neil; Malatesta, Lorenzo; Nordvall Forsberg, Fredrik.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Positive inductive-recursive definitions

AU - Ghani, Neil

AU - Malatesta, Lorenzo

AU - Nordvall Forsberg, Fredrik

PY - 2013/8/8

Y1 - 2013/8/8

N2 - We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.

AB - We introduce a new theory of data types which allows for the definition of data types as initial algebras of certain functors Fam ℂ → Fam ℂ. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer’s theory of inductive-recursive definitions within which ℂ had to be discrete – our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer’s work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer’s development). We show how these codes are interpreted as functors on Famℂ and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer’s set-theoretic model to our setting.

KW - data type

KW - generalisation

KW - inductive-recursive definitions

KW - initial algebras

KW - natural transformations

KW - nested data

KW - new theory

KW - set-theoretic models

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

UR - https://coalg.org/

U2 - 10.1007/978-3-642-40206-7_3

DO - 10.1007/978-3-642-40206-7_3

M3 - Conference contribution book

SN - 9783642402050

T3 - Lecture Notes in Computer Science

SP - 19

EP - 33

BT - Algebra and Coalgebra in Computer Science

A2 - Heckel, Reiko

A2 - Milius, Stefan

CY - Berlin

ER -