El Charity Development Group, investigador del Departamento de Ciencia Computacional de la Universidad de Calgary en Canadá, ha desarrollado Charity, un lenguaje de programación funcional basado en la teoría de tipos categóricos fuertes. Este lenguaje se divide en dos subclases: tipos de datos inductivos, construidos mediante constructores, y tipos de datos coinductivos, desglosados por destructores. Los programas en Charity se expresan mediante folds (catamorfismos) y unfolds (anamorfismos). Entre sus características principales destaca que es puro, soporta evaluación lazy (diferida), es de orden superior y todas las computaciones terminan (excepto por entrada del usuario). El lenguaje está diseñado para proporcionar un marco elegante y puro para el desarrollo de software, la enseñanza y la investigación de lenguajes, facilitando el razonamiento sobre programas y siendo altamente adecuado para especificación, transformación y verificación de código.
Charity: lenguaje de programación funcional basado en teoría de categorías
