Church numerals are a functional encoding of natural numbers. In the pure (untyped) lambda calculus, the definition of certain operations on Church numerals (addition, multiplication, etc) can be expressed “naturally”, in the sense of easy-to-understand and re-use of previously defined values. I’ve tried encoding these definitions in Haskell but the Rank-n type system infers rather strange types for numerals and operators. In his paper on System F, Reynolds suggested a polymorphic type for Church numerals and for arithmetic expressions. The way he defined them is not the same as the “natural” one (which can be expressed in System F as well). I have found that it can be expressed in Haskell (with some extra trickery) but it cannot be expressed in Agda (due to restrictions on impredicativity). I wonder if there is a type more general than Reynolds’ that is more specific than the one inferred by Haskell’s.

I have an interest in how to express programs more “naturally” and on the question of which features of the type system can help to achieve that. I found Haskell’s Rank-n system and Agda’s predicativity a hurdle for this case study. There are several proposals for making type inference possible with less and less type annotations (MLF, HMF, etc). For my PhD, I’m learning about types in programming and about the role of type checking and type inference. I’m curious about the limits of inference (not checking) and about the mechanisms that let me express types and functions in a more “natural” way.