Polymorphic Types in Haskell without Constructors?
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.
Research Blog
Substraction not Definable in Simply Typed Lambda Calculus
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.
Zipping Half of a List with Its Reversal
Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.
A Haskell Quine
A Haskell quine. That is, a program whose output is itself.
S Combinator is Injective
Do you know that the S combinator is injective? I have a simple algebraic proof and Nakano actually constructed its inverse.