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.
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.
primrec :: (N -> b -> b) -> b -> N -> b. Therefore, predecessor does not get the type pred :: N a -> N a either.
Developing Programs and Proofs Spontaneously using GADT