In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total:
- complete case analysis
- covariant type recursion (type constructor should not appear in negative position in a constructor argument)
- structural recursion
But with these rules I can still have an infinite loop:
data Fix f = Fix (f (Fix f)) data Bad r = Bad (r -> r) bad :: Fix Bad -> Fix Bad bad b = case b of Fix t -> case t of Bad f -> f b nonTotal = bad (Fix (Bad bad))
Where is my mistake? Should all type variables also only appear covariantly? Or is the "covariant type recursion" condition more strict?