Charity is based on the theory of strong categorical datatypes. These are divided into two subclasses: the inductive datatypes (built up by constructors in the familiar way) and the coinductive datatypes (broken down by destructors). Programs over these datatypes are expressed by folds (catamorphisms) and by unfolds (anamorphisms), respectively.
We list some, but not all, of Charity's features below:
Last modified 16 December 2024