On Sun, May 30, 2010 at 4:08 AM, wren ng thornton <wren@freegeek.org> wrote:

Jason Dagit wrote:

In Church's ė-calc the types are ignored,

Not so. Church-style lambda calculus is the one where types matter; Curry-style is the one that ignores types and evaluates as if it were the untyped lambda calculus.

Church encodings are based on the untyped LC rather than Church's simply-typed LC however, which is why they don't typecheck with Hindley--Milner.