I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.
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.
I was trying to simulate church numerals and primitive recursion in second rank polymorphism of Haskell. However, polymorphic types in Haskell can only be instantiated with monomorphic types.
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.