30 May
2010
30 May
'10
7:08 a.m.
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