6 ms·

I thought the same thing for a long time, I found s-expressions very elegant. Then I discovered lambda-calculus, with its scary syntax but based on a process I

I thought the same thing for a long time, I found s-expressions very elegant. Then I discovered lambda-calculus, with its scary syntax but based on a process I could understand, text-rewriting. So I had the idea to explore the lambda-calculus using s-expressions and patiently rebuilt booleans, pairs, lists, recursion and beyond a real complete Turing language, for instance: - http://lambdaway.free.fr/lambdawalks http://lambdaway.free.fr/lambdawalks - http://lambdaway.free.fr/lambdawalks/?view=lambdacode5 http://lambdaway.free.fr/lambdawalks/?view=lambdacode5 No need for cons, car, cdr and other historical names. We can rebuild everything from scratch, from abstractions and applications. No need for Lisp, Scheme, Common Lisp and other Clojure, even if they remain excellent examples. So in my opinion the Maxwell equations of computation are to be seen more in the lambda-calculus than in LISP and its dialects. We just need to make the syntax a little more human.

martyalain 4y ago
About "We just need to make the syntax a little more human", see for instance http://lambdaway.free.fr/lambdawalks/?view=sierpinsky4 http://lambdaway.free.fr/lambdawalks/?view=sierpinsky4
jerf 4y ago
For the reasons you give, it is perhaps more reasonable to say that Lisp is a Maxwell's Equations of software. But there are several. Forth has another reasonable claim to it, despite unpopularity, and Turing Machines have a claim too, despite their extreme unpopularity as a programming methodology. I don't know array languages well enough to know but I bet they have one too. There isn't really a unique set of Maxwell's equations in software.
- kragen 4y ago
  i wasn't able to get a runnable forth to less than a couple of pages written in itself https://github.com/kragen/stoneknifeforth https://github.com/kragen/stoneknifeforth but schönfinkel's ski-combinators are maybe the simplest practical basis s f g x → f x (g x) k a b → a i = s k k (one of many possible definitions) maybe wolfram knows of a simpler alternative my favorite is abadi and cardelli's object-calculus on which i based bicicleta. it has two reduction rules rather than the λ-calculus's one. using a hybrid of bicicleta's syntax and abadi and cardelli's {f = ς(v)b, g = ς(v)c, ...}{f = ς(v)d} → {f = ς(v)d, g = ς(v)c, ...} {f = ς(v)b, g = ς(v)c, ...}.f → b[{f = ς(v)b, g = ς(v)c, ...}/v] the first of these derives an inherited object with a new definition for method f. the second one invokes method f on an object, which is evaluated by replacing its self-variable v with the object itself throughout its body, using the standard β-reduction semantics with α-renaming that we're familiar with from the λ-calculus (b[x/y] means b but with x replacing y) despite the simplicity of the semantics the ς-calculus is enormously more usable for actually writing down functions than the λ-calculus. here's factorial(10) in the notation above (untested) {fac = ς(env){ n = ς(_)3, return = ς(o) (o.n < 2).if_true{ then = ς(_)1 else = ς(_)o.n * env.fac{n = ς(_)o.n - 1}.return }.return } }.fac{n = ς(10)}.return bicicleta has a lot of syntactic sugar which reduces this to (tested) {env: fac = {fac: arg1 = 3 '()' = (fac.arg1 < 2).if_true( then = 1 else = fac.arg1 * env.fac(fac.arg1 - 1) ) }}.fac(10) in particular to be able to define infix operators inside the language, bicicleta rewrites x * y as x.'*'{arg1 = y}.'()' and analogously for -, <, etc. they published a bunch of papers and a book on this but they were more interested in static typing than anything else. a paper on one imperative variation of the thing is http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf you can implement a turing machine in a few lines of c, making it internally simpler than the other alternatives, but as you point out it's unusable except as a compilation target or to prove theorems about
  - gradschool 4y ago
    > maybe wolfram knows of a simpler alternative Wolfram on combinators: https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view/ https://writings.stephenwolfram.com/2020/12/combinators-a-ce... not any simpler, but maybe these are: https://en.wikipedia.org/wiki/Iota_and_Jot https://en.wikipedia.org/wiki/Iota_and_Jot
    - kragen 4y ago
      oh yeah, how could I forget iota and jot, that was stupid of me
  - Gordonjcp 4y ago
    > but schönfinkel's ski-combinators are maybe the simplest practical basis Okay, but how much code goes into creating those operators?
    - kragen 4y ago
      it depends on what you're implementing them in, but in a term-rewriting language all you need is the two lines above. in js you need to implement some kind of term-rewriting. in 02006 i wrote a compiler from λ-calculus (using \ for λ, so you can write for example \x.\y.x for λx.λy.x, which is equivalent to the k combinator) to an augmented sk-combinator language in js that's at http://canonical.org/~kragen/tmp/sk.html http://canonical.org/~kragen/tmp/sk.html the definitions of s and k in it are S: [3, function(f, g, x) { return App(App(f, x), App(g, x)) }], K: [2, function(k, _) { return Ind(k) }], which are used as templates for matching by the 33-line-long sk_reduce function, which i'll spare you here the λ-calculus parser, the compiler from λ-calculus to sk-combinators, the sk-combinator parser, and the sk-combinator evaluator together are 391 lines of js if you just want to define the s and k combinators in js they look like this s = f => g => x => f(x)(g(x)) k = a => b => a but that is depending on the js interpreter to do the actual evaluation more recently i implemented a term-rewriting language in i386 assembly, it's about 800 bytes and 400 instructions: http://canonical.org/~kragen/sw/dev3/qfitzah.s http://canonical.org/~kragen/sw/dev3/qfitzah.s but i haven't quite figured out how to handle arithmetic, i/o, and variadic lists i think you could probably implement sk combinatory logic in about half a page of c if you were okay with leaking memory, you don't really need the flexibility of variadic lists and arbitrary identifiers in the sk-combinator language. every term is either a function application (of one function to one argument), s, or k
mannykannot 4y ago
I was going to say I had heard that this was the intention of Lisp's creators, then I thought I had better check, and immediately found this: Lisp had assignments and goto before it had recursion, and started as a dialect of Fortran! It was only later that Lisp programmers investigated the benefits of pure functions. Lisp was not based on lambda calculus, but rather Kleene's work on recursive functions. At the time, McCarthy had heard of lambda calculus but had not yet studied it! https://crypto.stanford.edu/~blynn/lambda/lisp.html https://crypto.stanford.edu/~blynn/lambda/lisp.html
- kazinator 4y ago
  The list processing in Lisp was inspired by FLPL: Fortran List Processing Language. This was more like a library of Fortran routines than a language, but in 1958 the term library for routines of code didn't even exist. Making new words of any kind was language development. FLPL already used the CAR and CDR terminology in its naming, with extra characters: XCARF and XCDRF (and others). The "extract CAR function" and "extract CDR function".
- bmitc 4y ago
  As far as I understand, McCarthy was into Godel, recursive functions, mathematics, and AI in trying to create Lisp to study these, not so much computability and the like. I think that's at least one line of thinking that causes people to say that McCarthy discovered Lisp instead of inventing it.
alexisread 4y ago
Nice take on lambda calc! It looks like you're making use of beta-reduction for the eval engine. Shen has a more formal take on lambda calc, and I think it's useful for more advanced constructs like type checking. Shen actually uses K-lambda (a lispish version of lambda calc) as part of it's compiler Sequent-calc->Prolog->Shen->K-lambda->VM: https://shenlanguage.org/TBoS/tbos_170.html https://shenlanguage.org/TBoS/tbos_170.html
- mattgreenrocks 4y ago
  This is really cool, thanks for linking that.
  - martyalain 4y ago
    My first goal was to write in a wiki using a light and extended HTML. I then discovered LISP and lambda-calculus. I built an "inverted" evaluator working directly on s-expressions (without AST), ignoring words (which therefore did not have to be protected by apostrophes and quotation marks), like in basic HTML. I can thus write wiki pages that are lambdatalk programs, mixing pure text and code effortlessly. It's my all-purpose tool.
    - all2 4y ago
      Do you have a write up on this tool somewhere? This sounds really cool!
      - martyalain 4y ago
        Thank you, everything starts in this page http://lambdaway.free.fr/lambdawalks http://lambdaway.free.fr/lambdawalks
- voxl 4y ago
  How is beta reduction not "formal"???
  - 4y ago
User23 4y ago
No need for those pesky variable names that make term rewriting clunk either[1]! The entire hygiene problem just disappears. Your style guide section on naming will also be greatly simplified. [1] https://en.wikipedia.org//wiki/De_Bruijn_index https://en.wikipedia.org//wiki/De_Bruijn_index
- martyalain 4y ago
  I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/ https://tromp.github.io/) But I don't despair of getting there one day...
- deleted 4y ago
  [deleted]
tromp 4y ago
I agree that Maxwell’s Equations of Software should be based on lambda calculus, the binary version of which [1] admits a much more concise 29 byte self-interpreter (λ11)(λλλ1(λλλλ3(λ5(3(λ2(3(λλ3(λ1 2 3)))(4(λ4(λ3 1(2 1))))))(1(2(λ1 2))(λ4(λ4(λ2(1 4)))5))))(3 3)2)(λ1((λ1 1)(λ1 1))) [1] https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html
- martyalain 4y ago
  I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/ https://tromp.github.io/) But I don't despair of getting there one day...
  - qsort 4y ago
    A picture is worth a thousand words: https://en.wikipedia.org/wiki/De_Bruijn_index#/media/File:De_Bruijn_index_illustration_1.svg https://en.wikipedia.org/wiki/De_Bruijn_index#/media/File:De... It's literally just notation: - It doesn't matter how you name variables. (if you want to sound cool: "lambda terms are invariant under alpha-conversion") - Each new variable introduces a scope. - Therefore, how scopes are nested defines the entire expression. - Instead of the usual way, we represent scopes with numbers, with the index representing "how nested the scope is". Imagine it's python, and you're pressing tab that many times.
    - pierrebai 4y ago
      Syntax and layout ware worth yet a few more orders of magnitude of words. But that argument has slipped past LISPers forever. I'll just let them keep scratching their heads why Python got so popular when LISP was around for so long and is /clearly/ superior.
      - lispm 4y ago
        I don't think LISPers are scratching their head about this. Lisp syntax is optimized towards meta-programming. Generating and processing code is built-in and supported with central mechanisms: READ, EVAL, PRINT, s-expressions, macros, ... Python is optimized towards simple pseudo-code like imperative OOP. That's easier for most programmers.
solomatov 4y ago
I would change it a bit. Lambda calculus (in Martin-Lof type theory) are Maxwell equations of logic. But, lambda calculus has very little real use in programming. There should be something else here.
justinhj 4y ago
The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy extends roughly to lambda calculus and a lisp system
- voxl 4y ago
  The Curry-Howard Correspondence is about proof systems. You would have a very hard time finding a proof theorist that says it's okay to have an undecidable proof checker or an inconsistent one. For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. Perhaps a para-consistent logic might work, but we're getting very exotic here.
  - justinhj 4y ago
    Interesting, thanks
  - hither_shores 4y ago
    > You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.
thrown_22 4y ago
>So I had the idea to explore the lambda-calculus using s-expressions and patiently rebuilt booleans, pairs, lists, recursion and beyond a real complete Turing language, for instance: Syntax is not semantics. The only thing that s-expressions do that is mathematically interesting is make the abstract syntax tree of expressions explicit in a way that standard notation does not. The whole point of them is that they make string rewriting into tree rewriting which is vastly easier and makes writing your own DSLs a breeze. From a practical point of view they are also the simplest way to serialize any expression which is why I can type them out in a text only comment as they are. Meanwhile doing the same with a math (or lambda calculus) expression requires a type setting system like latex to be understandable. Lisp has decided that application is nameless in its syntax which means that things like ((lambda (x) (+ x 1)) 2) work when semantically they mean (apply (lambda (x) (+ x 1)) 2). This makes programming with multivariable functions very clean but partial application incredibly messy, e.g. ((((lambda (x) (lambda (y) (lambda (z) (+ x y z)))) 1) 2) 3). This is not something that can be fixed because the ABS of partial application when thought of as a tree is indeed very messy. The only reason why it works in languages like Haskell as well as it does is that as long as you only have single variable function - goodbye thunks and multivariable functions - you can treat the partial application trees as a list instead. You can of course do the same in lisp using a DSL: '(partial ((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4)) But it doesn't fit very well with the rest of the language and feel quite pointless.
- martyalain 4y ago
  @thrown: This makes programming with multivariable functions very clean but partial application incredibly messy In lambdatalk the implementation of lambdas does not make them closures (no free variables) but is such that they accept de facto partial application and a number of values higher than the number of arguments. This compensates for the lack of closure. So for instance: ((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4)) is written this way {{{{{lambda {x y z w} {+ x y z w}} 1} 2} 3} 4} -> 10 and obviously {{lambda {x y z w} {+ x y z w}} 1 2 3 4} -> 10

martyalain 4y ago

About "We just need to make the syntax a little more human", see for instance http://lambdaway.free.fr/lambdawalks/?view=sierpinsky4 http://lambdaway.free.fr/lambdawalks/?view=sierpinsky4

jerf 4y ago

For the reasons you give, it is perhaps more reasonable to say that Lisp is a Maxwell's Equations of software. But there are several. Forth has another reasonable claim to it, despite unpopularity, and Turing Machines have a claim too, despite their extreme unpopularity as a programming methodology. I don't know array languages well enough to know but I bet they have one too. There isn't really a unique set of Maxwell's equations in software.

kragen 4y ago
i wasn't able to get a runnable forth to less than a couple of pages written in itself https://github.com/kragen/stoneknifeforth https://github.com/kragen/stoneknifeforth but schönfinkel's ski-combinators are maybe the simplest practical basis s f g x → f x (g x) k a b → a i = s k k (one of many possible definitions) maybe wolfram knows of a simpler alternative my favorite is abadi and cardelli's object-calculus on which i based bicicleta. it has two reduction rules rather than the λ-calculus's one. using a hybrid of bicicleta's syntax and abadi and cardelli's {f = ς(v)b, g = ς(v)c, ...}{f = ς(v)d} → {f = ς(v)d, g = ς(v)c, ...} {f = ς(v)b, g = ς(v)c, ...}.f → b[{f = ς(v)b, g = ς(v)c, ...}/v] the first of these derives an inherited object with a new definition for method f. the second one invokes method f on an object, which is evaluated by replacing its self-variable v with the object itself throughout its body, using the standard β-reduction semantics with α-renaming that we're familiar with from the λ-calculus (b[x/y] means b but with x replacing y) despite the simplicity of the semantics the ς-calculus is enormously more usable for actually writing down functions than the λ-calculus. here's factorial(10) in the notation above (untested) {fac = ς(env){ n = ς(_)3, return = ς(o) (o.n < 2).if_true{ then = ς(_)1 else = ς(_)o.n * env.fac{n = ς(_)o.n - 1}.return }.return } }.fac{n = ς(10)}.return bicicleta has a lot of syntactic sugar which reduces this to (tested) {env: fac = {fac: arg1 = 3 '()' = (fac.arg1 < 2).if_true( then = 1 else = fac.arg1 * env.fac(fac.arg1 - 1) ) }}.fac(10) in particular to be able to define infix operators inside the language, bicicleta rewrites x * y as x.'*'{arg1 = y}.'()' and analogously for -, <, etc. they published a bunch of papers and a book on this but they were more interested in static typing than anything else. a paper on one imperative variation of the thing is http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf http://lucacardelli.name/Papers/PrimObjImpSIPL.A4.pdf you can implement a turing machine in a few lines of c, making it internally simpler than the other alternatives, but as you point out it's unusable except as a compilation target or to prove theorems about
- gradschool 4y ago
  > maybe wolfram knows of a simpler alternative Wolfram on combinators: https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view/ https://writings.stephenwolfram.com/2020/12/combinators-a-ce... not any simpler, but maybe these are: https://en.wikipedia.org/wiki/Iota_and_Jot https://en.wikipedia.org/wiki/Iota_and_Jot
  - kragen 4y ago
    oh yeah, how could I forget iota and jot, that was stupid of me
- Gordonjcp 4y ago
  > but schönfinkel's ski-combinators are maybe the simplest practical basis Okay, but how much code goes into creating those operators?
  - kragen 4y ago
    it depends on what you're implementing them in, but in a term-rewriting language all you need is the two lines above. in js you need to implement some kind of term-rewriting. in 02006 i wrote a compiler from λ-calculus (using \ for λ, so you can write for example \x.\y.x for λx.λy.x, which is equivalent to the k combinator) to an augmented sk-combinator language in js that's at http://canonical.org/~kragen/tmp/sk.html http://canonical.org/~kragen/tmp/sk.html the definitions of s and k in it are S: [3, function(f, g, x) { return App(App(f, x), App(g, x)) }], K: [2, function(k, _) { return Ind(k) }], which are used as templates for matching by the 33-line-long sk_reduce function, which i'll spare you here the λ-calculus parser, the compiler from λ-calculus to sk-combinators, the sk-combinator parser, and the sk-combinator evaluator together are 391 lines of js if you just want to define the s and k combinators in js they look like this s = f => g => x => f(x)(g(x)) k = a => b => a but that is depending on the js interpreter to do the actual evaluation more recently i implemented a term-rewriting language in i386 assembly, it's about 800 bytes and 400 instructions: http://canonical.org/~kragen/sw/dev3/qfitzah.s http://canonical.org/~kragen/sw/dev3/qfitzah.s but i haven't quite figured out how to handle arithmetic, i/o, and variadic lists i think you could probably implement sk combinatory logic in about half a page of c if you were okay with leaking memory, you don't really need the flexibility of variadic lists and arbitrary identifiers in the sk-combinator language. every term is either a function application (of one function to one argument), s, or k

mannykannot 4y ago

I was going to say I had heard that this was the intention of Lisp's creators, then I thought I had better check, and immediately found this: Lisp had assignments and goto before it had recursion, and started as a dialect of Fortran! It was only later that Lisp programmers investigated the benefits of pure functions. Lisp was not based on lambda calculus, but rather Kleene's work on recursive functions. At the time, McCarthy had heard of lambda calculus but had not yet studied it! https://crypto.stanford.edu/~blynn/lambda/lisp.html https://crypto.stanford.edu/~blynn/lambda/lisp.html

kazinator 4y ago
The list processing in Lisp was inspired by FLPL: Fortran List Processing Language. This was more like a library of Fortran routines than a language, but in 1958 the term library for routines of code didn't even exist. Making new words of any kind was language development. FLPL already used the CAR and CDR terminology in its naming, with extra characters: XCARF and XCDRF (and others). The "extract CAR function" and "extract CDR function".
bmitc 4y ago
As far as I understand, McCarthy was into Godel, recursive functions, mathematics, and AI in trying to create Lisp to study these, not so much computability and the like. I think that's at least one line of thinking that causes people to say that McCarthy discovered Lisp instead of inventing it.

alexisread 4y ago

Nice take on lambda calc! It looks like you're making use of beta-reduction for the eval engine. Shen has a more formal take on lambda calc, and I think it's useful for more advanced constructs like type checking. Shen actually uses K-lambda (a lispish version of lambda calc) as part of it's compiler Sequent-calc->Prolog->Shen->K-lambda->VM: https://shenlanguage.org/TBoS/tbos_170.html https://shenlanguage.org/TBoS/tbos_170.html

mattgreenrocks 4y ago
This is really cool, thanks for linking that.
- martyalain 4y ago
  My first goal was to write in a wiki using a light and extended HTML. I then discovered LISP and lambda-calculus. I built an "inverted" evaluator working directly on s-expressions (without AST), ignoring words (which therefore did not have to be protected by apostrophes and quotation marks), like in basic HTML. I can thus write wiki pages that are lambdatalk programs, mixing pure text and code effortlessly. It's my all-purpose tool.
  - all2 4y ago
    Do you have a write up on this tool somewhere? This sounds really cool!
    - martyalain 4y ago
      Thank you, everything starts in this page http://lambdaway.free.fr/lambdawalks http://lambdaway.free.fr/lambdawalks
voxl 4y ago
How is beta reduction not "formal"???
- 4y ago

User23 4y ago

No need for those pesky variable names that make term rewriting clunk either[1]! The entire hygiene problem just disappears. Your style guide section on naming will also be greatly simplified. [1] https://en.wikipedia.org//wiki/De_Bruijn_index https://en.wikipedia.org//wiki/De_Bruijn_index

martyalain 4y ago
I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/ https://tromp.github.io/) But I don't despair of getting there one day...
deleted 4y ago
[deleted]

tromp 4y ago

I agree that Maxwell’s Equations of Software should be based on lambda calculus, the binary version of which [1] admits a much more concise 29 byte self-interpreter (λ11)(λλλ1(λλλλ3(λ5(3(λ2(3(λλ3(λ1 2 3)))(4(λ4(λ3 1(2 1))))))(1(2(λ1 2))(λ4(λ4(λ2(1 4)))5))))(3 3)2)(λ1((λ1 1)(λ1 1))) [1] https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html

martyalain 4y ago
I agree with you, but so far I have never been able to get into the logic of de Bruijn's clues. As for example John Tromp knows how to do. (https://tromp.github.io/ https://tromp.github.io/) But I don't despair of getting there one day...
- qsort 4y ago
  A picture is worth a thousand words: https://en.wikipedia.org/wiki/De_Bruijn_index#/media/File:De_Bruijn_index_illustration_1.svg https://en.wikipedia.org/wiki/De_Bruijn_index#/media/File:De... It's literally just notation: - It doesn't matter how you name variables. (if you want to sound cool: "lambda terms are invariant under alpha-conversion") - Each new variable introduces a scope. - Therefore, how scopes are nested defines the entire expression. - Instead of the usual way, we represent scopes with numbers, with the index representing "how nested the scope is". Imagine it's python, and you're pressing tab that many times.
  - pierrebai 4y ago
    Syntax and layout ware worth yet a few more orders of magnitude of words. But that argument has slipped past LISPers forever. I'll just let them keep scratching their heads why Python got so popular when LISP was around for so long and is /clearly/ superior.
    - lispm 4y ago
      I don't think LISPers are scratching their head about this. Lisp syntax is optimized towards meta-programming. Generating and processing code is built-in and supported with central mechanisms: READ, EVAL, PRINT, s-expressions, macros, ... Python is optimized towards simple pseudo-code like imperative OOP. That's easier for most programmers.

solomatov 4y ago

I would change it a bit. Lambda calculus (in Martin-Lof type theory) are Maxwell equations of logic. But, lambda calculus has very little real use in programming. There should be something else here.

justinhj 4y ago

The Curry-Howard correspondence suggests the analogy of computation with lambda calculus and logical proof systems. As a non-expert it seems that same analogy extends roughly to lambda calculus and a lisp system

voxl 4y ago
The Curry-Howard Correspondence is about proof systems. You would have a very hard time finding a proof theorist that says it's okay to have an undecidable proof checker or an inconsistent one. For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. Perhaps a para-consistent logic might work, but we're getting very exotic here.
- justinhj 4y ago
  Interesting, thanks
- hither_shores 4y ago
  > You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent. It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.

thrown_22 4y ago

>So I had the idea to explore the lambda-calculus using s-expressions and patiently rebuilt booleans, pairs, lists, recursion and beyond a real complete Turing language, for instance: Syntax is not semantics. The only thing that s-expressions do that is mathematically interesting is make the abstract syntax tree of expressions explicit in a way that standard notation does not. The whole point of them is that they make string rewriting into tree rewriting which is vastly easier and makes writing your own DSLs a breeze. From a practical point of view they are also the simplest way to serialize any expression which is why I can type them out in a text only comment as they are. Meanwhile doing the same with a math (or lambda calculus) expression requires a type setting system like latex to be understandable. Lisp has decided that application is nameless in its syntax which means that things like ((lambda (x) (+ x 1)) 2) work when semantically they mean (apply (lambda (x) (+ x 1)) 2). This makes programming with multivariable functions very clean but partial application incredibly messy, e.g. ((((lambda (x) (lambda (y) (lambda (z) (+ x y z)))) 1) 2) 3). This is not something that can be fixed because the ABS of partial application when thought of as a tree is indeed very messy. The only reason why it works in languages like Haskell as well as it does is that as long as you only have single variable function - goodbye thunks and multivariable functions - you can treat the partial application trees as a list instead. You can of course do the same in lisp using a DSL: '(partial ((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4)) But it doesn't fit very well with the rest of the language and feel quite pointless.

martyalain 4y ago
@thrown: This makes programming with multivariable functions very clean but partial application incredibly messy In lambdatalk the implementation of lambdas does not make them closures (no free variables) but is such that they accept de facto partial application and a number of values higher than the number of arguments. This compensates for the lack of closure. So for instance: ((lambda (x)) (lambda (y)) (lambda (z)) (lambda (w) (+ x y z w))) (1 2 3 4)) is written this way {{{{{lambda {x y z w} {+ x y z w}} 1} 2} 3} 4} -> 10 and obviously {{lambda {x y z w} {+ x y z w}} 1 2 3 4} -> 10