3 ms·

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 lin

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.