4 ms·

iiuc, the dichotomy "programming language vs. type system" doesn't hold for type-theoretic programming. E.g., languages based on System F (like Haskell) are bas

iiuc, the dichotomy "programming language vs. type system" doesn't hold for type-theoretic programming. E.g., languages based on System F (like Haskell) are based on a programming language that is inherently typed.

somewhereoutth 7y ago
Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of pathological statements have been disqualified, but perhaps some baby has gone out with the bathwater? To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.
- 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 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 ago
      You 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 ago
        The 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.

somewhereoutth 7y ago

Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of pathological statements have been disqualified, but perhaps some baby has gone out with the bathwater? To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.

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 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 ago
    You 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 ago
      The 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.