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.
-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe