5 ms·

I would say it doesn't have a formal 100% unambiguous definition, but it's certainly _more_ well-defined than OOP: a functional programming language is one whic

I would say it doesn't have a formal 100% unambiguous definition, but it's certainly _more_ well-defined than OOP: a functional programming language is one which is based on lambda calculus.

Rochus 5y ago
Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? OOP is just another way to organize code. Human language is unsuitable for "glass clear", unambiguous definitions, just because of its inherent fuzziness (which is nota bene an essential property for efficient communication).
- ebingdom 5y ago
  > Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? Not really. FP has an obvious connection to lambda calculus. Many OOP languages don't even have a straightforward notion of "function", which is what lambda calculus is all about.
  - Rochus 5y ago
    Did you have a look at e.g. https://www.amazon.com/Theory-Objects-Monographs-Computer-Science/dp/0387947752 https://www.amazon.com/Theory-Objects-Monographs-Computer-Sc...?
    - ebingdom 5y ago
      Yes, that's one of the most prominent in a long line of attempts at creating formal models of OOP. And in the preface, you'll find: > There is a well-established theory of functions, the λ-calculus, ... However, our theory of objects is self-contained; it is the first that does not require explicit reference to functions or procedures. So that answers your question in the negative and proves my point: no, not every language is based on lambda calculus.
      - Rochus 5y ago
        There are also different "schools of thought" for functional programming. That in itself is not a bad thing. The thread was about formal definitions; such are therefore available for those who need them.
  - Rochus 5y ago
    > Not really See e.g. Landin, P. J. (1965): A Correspondence between ALGOL 60 and Church's Lambda-notation.
- carapace 5y ago
  > Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? No. Prolog et. al. is based on Horn Clause representation and evaluated using something called SLD resolution. "Concatinative" languages (like Joy) are based on function composition (not application.) (FWIW, the Turing machine is not based on Lambda calculus. Not that TMs are a programming language.)
  - Rochus 5y ago
    Aren't turing machines and the lambda calculus equivalent, i.e. each can efficiently simulate the other?
    - carapace 5y ago
      They're equivalent, but not identical. Lots of formal systems are Turing complete (e.g. Wang Tiles) and so can compute the same results as each other. Wolfram goes on about this some. I sometimes wonder about the possible form of the "Platonic Ideal" is that each of these systems represent. George Spencer-Brown's Laws of Form seems to me to be the ultimate concrete example, but that's not a universally held opinion. :)
      - Rochus 5y ago
        But doesn't that mean you can create a corresponding lambda calculus based version of a programming language, such as Landin did in his 1965 paper?
        carapace 5y ago
        Of course, but you could do that with the other formal systems too. It's like Roman numerals vs. base-10 numerals, eh? "XXIII" and "23" both denote the same number (which may or may not exist depending on your metaphysical outlook) but neither notation can be said to be "the" notation.
        5y ago
kaba0 5y ago
How are expressions not based on lambda calculus in most “ordinary” languages? Yeah, they may side effect but at the same time lambda calculus itself is untyped, so is Haskell all that much closer to it over C++?
- tome 5y ago
  Many other languages are not expression based at all. for loops cannot be considered "lambda calculus", for example (although of course there is a translation of them into a lambda calculus equivalent).
  - kaba0 5y ago
    While they do have statements as well, they usually also have expressions, which are referentially transparent (and yeah I know it’s not the usage most people use, but it is the correct one: https://stackoverflow.com/questions/210835/what-is-referential-transparency https://stackoverflow.com/questions/210835/what-is-referenti... ). (They don’t employ currying though)
    - tome 5y ago
      I never quite understood Uday's objection. Any language can be referentially transparent if you consider it's denotation to be just its syntax. Then you can always replace equals with equals, but the only thing equal to an expression is the exact same sequence of characters! The whole point is to be referentially transparent with respect to as coarse a semantics as possible. Haskell gets some of the way there, yet even let x = e y = e in ... is not equivalent to let x = e y = x in ... if your semantics can distinguish expressions by the time they take to evaluate. Still (to address your original question) people do consider lambda calculi with effects, so if the expression-based fragment of an imperative language supports lambdas with lexical scoping then sure you could get away with saying that "their expression are based on lambda calculus".
      - kaba0 5y ago

I would say it doesn't have a formal 100% unambiguous definition, but it's certainly _more_ well-defined than OOP: a functional programming language is one which is based on lambda calculus.

Rochus 5y ago

Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? OOP is just another way to organize code. Human language is unsuitable for "glass clear", unambiguous definitions, just because of its inherent fuzziness (which is nota bene an essential property for efficient communication).

ebingdom 5y ago
> Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? Not really. FP has an obvious connection to lambda calculus. Many OOP languages don't even have a straightforward notion of "function", which is what lambda calculus is all about.
- Rochus 5y ago
  Did you have a look at e.g. https://www.amazon.com/Theory-Objects-Monographs-Computer-Science/dp/0387947752 https://www.amazon.com/Theory-Objects-Monographs-Computer-Sc...?
  - ebingdom 5y ago
    Yes, that's one of the most prominent in a long line of attempts at creating formal models of OOP. And in the preface, you'll find: > There is a well-established theory of functions, the λ-calculus, ... However, our theory of objects is self-contained; it is the first that does not require explicit reference to functions or procedures. So that answers your question in the negative and proves my point: no, not every language is based on lambda calculus.
    - Rochus 5y ago
      There are also different "schools of thought" for functional programming. That in itself is not a bad thing. The thread was about formal definitions; such are therefore available for those who need them.
- Rochus 5y ago
  > Not really See e.g. Landin, P. J. (1965): A Correspondence between ALGOL 60 and Church's Lambda-notation.
carapace 5y ago
> Isn't every existing programming language eventually based on (or at least traceable to) lambda calculus? No. Prolog et. al. is based on Horn Clause representation and evaluated using something called SLD resolution. "Concatinative" languages (like Joy) are based on function composition (not application.) (FWIW, the Turing machine is not based on Lambda calculus. Not that TMs are a programming language.)
- Rochus 5y ago
  Aren't turing machines and the lambda calculus equivalent, i.e. each can efficiently simulate the other?
  - carapace 5y ago
    They're equivalent, but not identical. Lots of formal systems are Turing complete (e.g. Wang Tiles) and so can compute the same results as each other. Wolfram goes on about this some. I sometimes wonder about the possible form of the "Platonic Ideal" is that each of these systems represent. George Spencer-Brown's Laws of Form seems to me to be the ultimate concrete example, but that's not a universally held opinion. :)
    - Rochus 5y ago
      But doesn't that mean you can create a corresponding lambda calculus based version of a programming language, such as Landin did in his 1965 paper?
      - carapace 5y ago
        Of course, but you could do that with the other formal systems too. It's like Roman numerals vs. base-10 numerals, eh? "XXIII" and "23" both denote the same number (which may or may not exist depending on your metaphysical outlook) but neither notation can be said to be "the" notation.
        5y ago

kaba0 5y ago

How are expressions not based on lambda calculus in most “ordinary” languages? Yeah, they may side effect but at the same time lambda calculus itself is untyped, so is Haskell all that much closer to it over C++?

tome 5y ago
Many other languages are not expression based at all. for loops cannot be considered "lambda calculus", for example (although of course there is a translation of them into a lambda calculus equivalent).
- kaba0 5y ago
  While they do have statements as well, they usually also have expressions, which are referentially transparent (and yeah I know it’s not the usage most people use, but it is the correct one: https://stackoverflow.com/questions/210835/what-is-referential-transparency https://stackoverflow.com/questions/210835/what-is-referenti... ). (They don’t employ currying though)
  - tome 5y ago
    I never quite understood Uday's objection. Any language can be referentially transparent if you consider it's denotation to be just its syntax. Then you can always replace equals with equals, but the only thing equal to an expression is the exact same sequence of characters! The whole point is to be referentially transparent with respect to as coarse a semantics as possible. Haskell gets some of the way there, yet even let x = e y = e in ... is not equivalent to let x = e y = x in ... if your semantics can distinguish expressions by the time they take to evaluate. Still (to address your original question) people do consider lambda calculi with effects, so if the expression-based fragment of an imperative language supports lambdas with lexical scoping then sure you could get away with saying that "their expression are based on lambda calculus".
    - kaba0 5y ago