4 ms·
No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. T
by 6gvONxR4sf7o 7y ago
No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. They’re very much related, and there’s a strong sense in which they are built on each other, but the kinds of programs available and what can be proved or guaranteed are different.
- somewhereoutth 7y agobut (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?
- throwaway17_17 7y agoYou are essentially identifying the semantic divergence between Church and Curry style types. Church-style or Intrinsically typed Lambda Calculus does not give any meaning to ill-typed expressions and there for beta-reduction can not proceed for these invalid expressions. Where as Curry-style or Extrinsically typed lambda calculus gives meaning to expression that do not consider the type alleged to be possessed by that expression.
- somewhereoutth 7y agoThe crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). Both are systems for proving type correctness of terms.