Inductive Type
Contents
Definition
Induction Principle
Coinduction Principle
Inductive Types
Church Data Type (iterative), in Ξ»2
Scott Data Type (case), in Ξ»2ΞΌ
Church-Scott Data Type (primitive recursive), in Ξ»2ΞΌ
Coinductive Types
ΞΌ
π + π
π, boolean.
π + A
Option, or maybe.
π + X
Church-Scott
[herman-geuvers-2014], [herman-geuvers-2015]
π + (A Γ X )
List.
Church-Scott
π + ( A Γ X Γ X )
Binary tree.
Church-Scott
A + ( A Γ X ) + ( X Γ X )
Lambda calculus.
[yigal-duppen-2000]
π + X + (β β X )
Ordinals.
π + ( X Γ Y )
F tree.
Ξ½
A Γ X
Stream.
Church-Scott
Ξ»2
Ξ»2ΞΌ
πΓ (A β X )
Deterministic automata.
A Γ (Bβ X )
W-types.
ΞΌ _.(π + A Γ X )
Colist.
β Γ (ΞΌ X.π + A Γ X )
Vector.
Polynomial Functors
Quotients of Polynomial Functors
The class of QPFs is closed under:
- composition
- quotients
- initial algebras
- final colagebras
In particular, finset and multiset are QPFs.
References
- Bahareh Afshari, Gerhard JΓ€ger, Graham E. Leigh. An Infinitary Treatment of Full ΞΌ-Calculus. 2019.
- Simon Hudon. Datatypes as Quotients of Polynomial Functors. 2019.
- Xavier Leroy. Sisyphus Happy: Infinite Data Types, Proofs by Coinduction, and Reactive Programming. 2019.
- Ambrus Kaposi. A Syntax for Higher Inductive Inductive Types (HIITs). 2018.
- Alexander Kurz. An Introduction to Coalgebra in Four Short Lectures and Two Long Appendices. 2018.
- Jakob Vidmar. Polynomial Functors and W-Types for Groupoids. 2018.
- Niels van der Weide. Higher Inductive Types. 2016.
- Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. Copatterns: Programming Infinite Structures by Observations. 2013.
- Michael Abbott, Thorsten Altenkirch, Neil Ghani1. Representing Nested Inductive Types Using W-Types. 2004.