30 May
2010
30 May
'10
3:33 p.m.
On Sun, May 30, 2010 at 4:08 AM, wren ng thornton
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.
Oh I see. Thanks for that correction. Jason