3 ms·
but (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 d
by somewhereoutth 7y ago
but (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.