4 ms·

I'm not who you replied to, however: - The original Lisp was based on mutable singly linked lists. Lambda calculus has no lists, except for Church-encoded ones

I'm not who you replied to, however: - The original Lisp was based on mutable singly linked lists. Lambda calculus has no lists, except for Church-encoded ones (just like lambda calculus only has Church encoded booleans and numbers). It also doesn't have mutability. - Later, Common Lisp (which was a unification of the Lisp variants that had descended from Lisp 1.5) also grew an object system, and it was implemented using dynamic scoping and dynamic typing. That stuff definitely has nothing to do with lambda calculus. If you want an implementation of the lambda calculus, you could try Haskell 98 or Standard ML. Those are based on System F [0], a kind of typed lambda calculus. [0]: https://en.wikipedia.org/wiki/System_F https://en.wikipedia.org/wiki/System_F

kazinator 2y ago
Though Lisp was originally implemented with lists that suported RPLACA and RPLACD functions for practical reasons, the interpretation of Lisp semantics in Lisp was specified (before Lisp was implemented) without using these functions.
tromp 2y ago
> The original Lisp was based on mutable singly linked lists. Lambda calculus has no lists, except for Church-encoded ones (just like lambda calculus only has Church encoded booleans and numbers). While Lambda calculus only has 1 argument functions, you can use those to encode lists [1] and numbers in many ways, including unary, binary, and ternary [2]. [1] https://en.wikipedia.org/wiki/Church_encoding#List_encodings https://en.wikipedia.org/wiki/Church_encoding#List_encodings [2] https://bruijn.marvinborner.de/std/Number_Ternary.bruijn.html https://bruijn.marvinborner.de/std/Number_Ternary.bruijn.htm...
- kazinator 2y ago
  Encodings built up within lambda calculus are not known to lambda calculus itself, and are ambiguous. There is no way to tell whether some encoding isn't just supposed to denote itself (the lambda calculus functional term that it is) rather than a number that it represents by convention.
  - tromp 2y ago
    > Encodings built up within lambda calculus are not known to lambda calculus itself, and are ambiguous. Which is why it's strange for trealira to single out Church encoded booleans and numbers.
    - trealira 2y ago
      I wasn't trying to single them out; I was saying that lambda calculus has only lambda terms and applications, whereas Lisp always natively supported mutable linked lists from the beginning. Coming back to that argument after a day, though, it admittedly seems like a weak argument; after all, Standard ML supports mutability and linked lists natively as well, and I gave that as an example of typed lambda calculus. Maybe a better argument is that it's dynamically typed, whereas I don't think there are dynamically typed formations of lambda calculus.
      - diligentClerk 2y ago
        The original lambda calculus had no type system at all, it was just a term rewriting system of variables and lambda abstractions with two rules: (\lambda a.M)N --> M[N/a] (\lambda a.M a) --> M In this sense we can say it is "dynamically typed" in that it has a single type, the type of lambda terms, although this seems like it sells short the memory safety guarantees associated to types in modern dynamically typed languages. This is the system that comes to mind for me when I think of "lambda calculus" because it is the one that was most important in the history of computability and logic, it can express the same computable functions as Turing machines. System F is not Turing complete.

kazinator 2y ago

Though Lisp was originally implemented with lists that suported RPLACA and RPLACD functions for practical reasons, the interpretation of Lisp semantics in Lisp was specified (before Lisp was implemented) without using these functions.

tromp 2y ago

> The original Lisp was based on mutable singly linked lists. Lambda calculus has no lists, except for Church-encoded ones (just like lambda calculus only has Church encoded booleans and numbers). While Lambda calculus only has 1 argument functions, you can use those to encode lists [1] and numbers in many ways, including unary, binary, and ternary [2]. [1] https://en.wikipedia.org/wiki/Church_encoding#List_encodings https://en.wikipedia.org/wiki/Church_encoding#List_encodings [2] https://bruijn.marvinborner.de/std/Number_Ternary.bruijn.html https://bruijn.marvinborner.de/std/Number_Ternary.bruijn.htm...

kazinator 2y ago
Encodings built up within lambda calculus are not known to lambda calculus itself, and are ambiguous. There is no way to tell whether some encoding isn't just supposed to denote itself (the lambda calculus functional term that it is) rather than a number that it represents by convention.
- tromp 2y ago
  > Encodings built up within lambda calculus are not known to lambda calculus itself, and are ambiguous. Which is why it's strange for trealira to single out Church encoded booleans and numbers.
  - trealira 2y ago
    I wasn't trying to single them out; I was saying that lambda calculus has only lambda terms and applications, whereas Lisp always natively supported mutable linked lists from the beginning. Coming back to that argument after a day, though, it admittedly seems like a weak argument; after all, Standard ML supports mutability and linked lists natively as well, and I gave that as an example of typed lambda calculus. Maybe a better argument is that it's dynamically typed, whereas I don't think there are dynamically typed formations of lambda calculus.
    - diligentClerk 2y ago
      The original lambda calculus had no type system at all, it was just a term rewriting system of variables and lambda abstractions with two rules: (\lambda a.M)N --> M[N/a] (\lambda a.M a) --> M In this sense we can say it is "dynamically typed" in that it has a single type, the type of lambda terms, although this seems like it sells short the memory safety guarantees associated to types in modern dynamically typed languages. This is the system that comes to mind for me when I think of "lambda calculus" because it is the one that was most important in the history of computability and logic, it can express the same computable functions as Turing machines. System F is not Turing complete.