3 ms·
When you mentioned lambda calculus I assumed you meant functions were to be added as a primitive executable type. Then you would logically have lists defined as
by James_K 2y ago
When you mentioned lambda calculus I assumed you meant functions were to be added as a primitive executable type. Then you would logically have lists defined as:
(define (cons a b) (lambda (x y) (x a b)))
(define nil (lambda (x y) (y)))
Which is problematic because you can write down the list-form of a lambda but not the actual value of it.
When you suggest the addition of an additional record type to the language because it's good from a software engineering perspective, I think this goes against the idea for this document (that the language should be entirely formal and ignore software engineering considerations). There are all sorts of things you might want types for, but I think the point here is to demonstrate that you can use lists for all of them.
> I think you don't know what you're talking about.
Rude.
- lisper 2y ago> Which is problematic because you can write down the list-form of a lambda but not the actual value of it. That's not true. Nothing prevents you from defining a serialization format for lambdas. That is in fact what all modern Lisps do. > When you suggest the addition of an additional record type to the language When did I suggest that? Pointing out that Bel doesn't have a record type is not the same as suggesting one should be added. Bel is intended to be a specification, not an implementation. > Rude. Do you think so? I was responding to this: > I think the lesson here is really that lisp is a convenient syntax but a lousy model for computation. Calling Lisp a "lousy model for computation" is not only objectively false -- Lisp is the foundation of all modern programming languages -- it also denigrates the work of hundreds of people over decades. Maybe that's not what you intended. Maybe you are simply ignorant. But I actually thought that mine was a pretty measured response.
- James_K 2y ago> That's not true. Nothing prevents you from defining a serialization format for lambdas. That is in fact what all modern Lisps do. If you have a list defined "al la lambda calculus" as a lambda term, you can't really write it down fully because to do that you'd need to write a lambda and a lambda is written in terms of lists and lists are written in terms of lambda. As an example: (a b) ;; is a shorthand for (a . (b . nil)) ;; and with lists that's where it ends ;; but with lambdas (a . b) ;; is a shorthand for (lambda (f g) (f a b)) ;; is a shorthand for (cons lambda (cons (cons f (cons g nil)) (cons (cons f (cons a (cons b nil)))))) ;; which expands to (lambda (f g) (f 'lambda (lambda (lambda (f g) (f 'f (lambda (f g) (f 'g nil)))) (f (f g) (lambda (f g) (f (lambda (f g) (f 'f (lambda (f g) (f 'a (lambda (f g) (f 'b nil)))))))))))) ;; which is a shorthand for ... You never reach the end of it. > Lisp is the foundation of all modern programming languages Not really. People like to say that lisp had a much greater influence than it actually did. If I called Smalltalk the "foundation of all modern programming languages", you'd instantly see that it isn't true. Lisp was one step taken by some people along one particular path, not the first or the last and hardly the foundation. > it also denigrates the work of hundreds of people over decades No it doesn't. If you think it does then name them. To my knowledge the people researching programming don't use list-based methods of computation because they are too complex and the people implementing programming languages don't use list-based methods of computation because that's not how hardware works. > Maybe you are simply ignorant Maybe you are simply rude.
- lisper 2y ago> If you have a list defined "al la lambda calculus" as a lambda term, you can't really write it down fully Here is an existence proof that you are wrong about that: https://flownet.com/ron/lambda-calculus.html https://flownet.com/ron/lambda-calculus.html > To my knowledge the people researching programming don't use list-based methods of computation The ignorance you display here is truly breathtaking. > Maybe you are simply rude. Yep, that's possible too.
- James_K 2y ago> The ignorance you display here is truly breathtaking. Remember when I said "if you disagree, give me an example of such research"? Now is the time to do that. > Here is an existence proof that you are wrong about that: No it isn't. Because they have lambda defined as an axiom. If you define lambda in terms of lists, and lists in terms of lambda, it's pretty trivial to say you have a circular reference on your hands.
- lisper 2y ago> Now is the time to do that. Sigh. https://www.amazon.com/Essentials-Programming-Languages-MIT-Press/dp/0262062798 https://www.amazon.com/Essentials-Programming-Languages-MIT-... > they have lambda defined as an axiom "They" is me -- I wrote that article. And no, "they" do not have lambda defined as an axiom. There are no axioms in that article because there are no proofs. It's just a demonstration of how you can do math using lambda calculus, with pairs being built along the way (and ultimately abandoned in favor of Church numerals) along with an actual implementation of a serializer for lambdas called lc-expand. If you don't see how that refutes your claim that "If you have a list defined "al la lambda calculus" as a lambda term, you can't really write it down fully" I'm not going to try to explain it to you. You are apparently beyond my ability to help.
- James_K 2y ago> https://www.amazon.com/Essentials-Programming-Languages-MIT- https://www.amazon.com/Essentials-Programming-Languages-MIT-... That is a textbook, not research. > "They" is me -- I wrote that article. Makes sense. The HTML elements are broken in some of the code snippets by the way. A few of & scattered about the place. > There are no axioms in that article because there are no proofs. Google "Curry-Howard correspondence". Computation is defined through axioms; you cannot compute without them. > You are apparently beyond my ability to help. I think you are just incapable of reading and processing ideas from other people without insulting them due to some sort of ego-trip where you imagine you are the messiah sent from heaven to educate us poor ingrates about programming when you clearly are not. Be less obnoxious in future and more open to new ideas.