Charity

A lazy higher-order functional programming language based on the concepts of category theory. It supports both inductive and co-inductive type definitions, and is terminating with the exception of pending inputs (this means it is not Turing-complete, but it is still useful and safe in that respect).

The following came from a discussion on LtU:

It's based on a core language (categorical combinators) which is easy to prove termination for but, instead of adding recursion and sugar, they only added sugar, so all Charity programs terminate except when blocking on input.

In Charity, strong constraints on the construction of data and the operators associated with them are the critical characteristic; all operations definable are total morphisms. (Algebraic) datatype definitions in Charity are not very different from ones in Haskell, but whereas Charity has a fold construct for each datatype, Haskell forces you to define it for yourself using recursion. So Charity short-circuits the step where you get a proof obligation for termination. Of course, you can do non-well-founded recursion in Haskell also, which is what gives the extra power and the possibility of divergence.