In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.
An indcutive type μF is simulated by
forall x . (F x -> x) -> x, while a coinductive type νF is simulatd by
exists x . (x -> F x, x). When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.
We can even define primitive recursion, only that it does not have the desired type
primrec :: (N -> b -> b) -> b -> N -> b. Therefore, predecessor does not get the type
pred :: N a -> N a either.