8 ms·

I used to be a fan of these languages like Lisp and Forth and Joy (and Factor and Haskell), but then I found that what I a really long for is just (untyped) lam

by js8 1y ago

I used to be a fan of these languages like Lisp and Forth and Joy (and Factor and Haskell), but then I found that what I a really long for is just (untyped) lambda calculus (as a universal language). (Combinatory logic is just a similar representation of lambda calculus, but the differences go away quickly once you start abstracting stuff.) I think expressing semantics of all (common) programming languages in lambda calculus would give us a solid foundation for automated program translation. And we should aim for that, the babel tower of languages doesn't really help anyone. The current issue I have is with type theory. So I am trying to embed notion of types directly into the lambda terms, so they would sort of "automatically typecheck" when composed. The crucial in this, in my opinion, are lambda terms that do not use lambda abstraction in their body, because you can think of these terms as a kind of mini-DSLs that have yet to be interpreted. Anyway, once we can translate calculus of constructions (and other common formal logics) into untyped lambda calculus, it will also help us doing automated theorem proving. It must be theoretically possible, but to my knowledge nobody has really done this sort of hardcore formalization.

procaryote 1y ago
Why specifically untyped?
- js8 1y ago
  Because it is the simplest thing we have, and has a pretty straightforward self-interpreter. It feels like you need a lot more metamathematics to deal with typed lambda calculus than with untyped one, and types are something that comes without a justification. Anyway, the idea is, if you have a language, you can think of source code written in the language as a giant lambda term, where you have all lambdas upfront and only composition in the body. A tree of symbols to be composed, essentially. And then to interpret this source code in a language, you supply definitions of the language's primitives as arguments to the source code term. Now if your language is typed, the primitives need to be chosen in such a way, so that the interpreted term (the source code applied to language primitives) fails to normalize if the program is not typed correctly. You can then have a correspondence between the primitives of the typed language that typecheck and simpler set of primitives of the same language used purely for computation, used under the assumption that the program typechecks. This correspondence "defines" the typing mechanism of your language (in untyped lambda terms).
  - tromp 1y ago
    > have all lambdas upfront and only composition in the body That is only possible for a very limited subset of lambda terms. For example, it's not possible for the one-point basis A = λx λy λz. x z (y (λw. z)) from which any closed lambda term can be constructed by composition.
    - js8 1y ago
      Yes, that's deliberate though. (I will call these "concrete" terms, because they lack abstraction in the body, but I am looking for a good name. In fact, no universal one-point basis can be expressed as a single term like that, you need a composition of two; the concrete property is not preserved in composition, although it might be preserved in weaker bases than S,K, such as B,C,K - kind of affine logic.) Anyway, the reason I am interested in concrete terms is I want to define typing judgements in ULC somehow. (In CoC, all mathematical questions can be rephrased as is there an object of given type T, and you need to be able to formalize questions somehow to formalize metamathematics.) An obvious definition of typing judgement in ULC would be: term x is of type B in a typed language A (both A and B are given terms) iff there exists a term x that satisfies Ax = B (the equality is judgemental after beta-normalization). However, this definition doesn't work, because a general term x can just disregard A and return B directly. But - I think if we restrict x to be a concrete term in the above definition (possibly with a given number of upfront lambdas - not sure if that is required), then I think we can make the definition to work. I also suspect concrete terms can be sort of "deconstructed from the outside". In general, we cannot resolve equality of terms, but I suspect that concrete terms can be analyzed (and quoted) within ULC. One thing I realized about your CoC implementation - I think you embed CoC into ULC in an indirect way, working with CoC terms in a quoted way. And that's fine, but what I want is to have CoC in ULC directly, i.e. have a base set of ULC terms for the primitives of CoC language. But that also can be thought of as the CoC interpreter being restricted to apply on concrete terms, giving them meaning by substituting the base inside. In other words, concrete terms are kind of "inside view" of quoting. (Maybe we should call them "data terms", because they effectively carry only data and no executable payload.) Having the concept of concrete terms in the ULC metalanguage can also help to define interaction to the external world, that you only accept data not executables, something that you kinda do through the "monadic" interface. (You need to "remember" that a term only accepts quoted data, it cannot be made explicit in ULC language. The advantage of concrete terms is they are independent on your choice of quoting operator.) Anyway, I am not sure if I am making sense, I am trying to grapple with this myself, so it's OK if you don't think concrete terms are a useful concept.
- jonathanstrange 1y ago
  The typed lambda calculus is not Turing complete.
  - js8 1y ago
    Not quite true, depends on the flavor of the type system you use. Church's simply typed is not, but other type systems are. I think one way to make it Turing complete is to add typing rule for Y combinator as an axiom to your simple type system, but I am not sure.
    - jonathanstrange 1y ago
      Yes, I had Church's simply typed lambda calculus in mind. You need to add a fix point combinator or general recursion.
tromp 1y ago
I implemented the Calculus of Constructions in untyped lambda calculus in order to shorten the 643 byte C program computing Loader's Number to 1850 bits (under 232 bytes) [1], as one of the milestones reached by my functional busy beaver function [2]. [1] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634 https://codegolf.stackexchange.com/questions/176966/golf-a-n... [2] https://oeis.org/A333479 https://oeis.org/A333479
- js8 1y ago
  I think this is great. I think you should write a paper on it. I suspect it might need some kind of commutative diagram proof, i.e. if you express things in CoC formalized within BLC you will get the same result as when you express in BLC formalized within CoC, I am not sure from the top of my head. (Kind of similar to showing that self-interpreting quoted interpreter on quoted program is the same as quoting the result of running the interpreter on the program.) And of course, this proof of equivalence should have formalization both in CoC (Lean?) and BLC. My hope is eventually someone writing a book on logic where the metalogic will be just untyped lambda calculus. Proofs will be just beta-reduction and judgemental equality. And everything will be in the form, let's study properties of these lambda terms that I came up with (the terms will of course represent some other logic such as CoC, simply typed LC, or even LC itself etc.).
CaptainOfCoit 1y ago
> And we should aim for that, the babel tower of languages doesn't really help anyone. What exactly do you mean with this? That the amount of programming languages available isn't actually helpful, it's detrimental?
- Mountain_Skies 1y ago
  Everyone should be free to unite behind my choices. It's obviously what is best for everyone.
  - js8 1y ago
    That's a rather cheap retort. I am not saying everybody should use raw untyped lambda calculus for their programming, just that we would all benefit if we could translate languages we use to and from it, because then we could interoperate with any other code, refactor it, etc.
    - actionfromafar 1y ago
      Isn’t structure lost in the compilation process? I mean, we already have bits and pieces of what you want, like an assembler to C decompiler, but the output isn’t very nice without the types. And how many languages can run on the CIL in dotnet. Say we create a CIL to lambda calculus compiler. Where do we go from there?
      - js8 1y ago
        A CIL to LC compiler is effectively an emulator of CIL in LC. That is, every primitive of CIL has a corresponding LC term, which operates on the CIL execution state. So then you can express functions from .NET standard library as terms in LC. Now let's say you do the same for JVM. Now you can start looking at all these lambda terms and search for some similarities. For example, you might notice that some list functions are equivalent if you transform the representation in a certain invertible way. This gives you a way to express functions from one standard library in the other. In general, I think we should try to translate wide variety of human programs into lambda calculus and then try to refactor/transform the lambda terms to spot the common patterns.
entaloneralie 1y ago
A lot of languages(including forth) maps really poorly to LC. Read some of the Forth writing on portability at all costs: http://www.ultratechnology.com/antiansi.htm http://www.ultratechnology.com/antiansi.htm
- tromp 1y ago
  Simple pure concatenative languages map quite well though [1]. [1] https://github.com/tromp/AIT/blob/master/ait/mlatu.lam https://github.com/tromp/AIT/blob/master/ait/mlatu.lam
  - entaloneralie 1y ago
    Joy, right? Not Forth. Conversion between spagetti stacks and pure stack programming(in which the stack contains numbers and no GC) has a massive translation cost if you go from LC to Forth and back.
    - js8 1y ago
      Forth is an imperative language and as such you will have to model memory state (at least) somehow, if you want to use purely functional language as a representation. But that's the cost of doing business. The thing is though, you don't translate to LC for performance, but for understanding. At any point, the LC evaluator might recognize a known subterm and replace it with a known equivalent. Depending on the goal, that might help to improve evaluation performance (skip known steps of beta reduction), reduce memory consumption (reduce size of the term), or improve readability (refactor code to use better known abstractions).
- skybrian 1y ago
  It's difficult to understand what they were actually doing, but reading between the lines, it sounds like an advantage of 'machine Forth' is writing some Forth words in assembly? I can see why that would run much faster for a jpeg decoder.
lambdaone 1y ago
Grounding programming languages in mathematics like this is essentially the goal of Strachey and Scott's denotational semantics, which has been very influential in programming language theory: https://en.wikipedia.org/wiki/Denotational_semantics https://en.wikipedia.org/wiki/Denotational_semantics
- bananaflag 1y ago
  All approaches to semantics of programming languages are mathematical, the denotational one is not "more mathematical" than the rest.
- js8 1y ago
  Not really a big fan, because the formalization of DS always left something desired, but I think a big difference with formalization in ULC is that ULC is (mostly) materialist while DS is structuralist. So the initial formalization into ULC can be automated - if you have semantics of your language already implemented as an interpreter in another language, you can use this as a starting point. With DS - I am not sure. I feel most people who build new languages don't provide DS specification.
deleted 1y ago
[deleted]
mighmi 1y ago
It's a real cool idea to compile everything down to lambda calculus and then you solve all semantics issues. (If something fits) you can convert 1:1, use general libraries in one language in others without loss etc. Ah, what a beautiful world it could be!

by js8 1y ago

procaryote 1y ago

Why specifically untyped?

js8 1y ago
Because it is the simplest thing we have, and has a pretty straightforward self-interpreter. It feels like you need a lot more metamathematics to deal with typed lambda calculus than with untyped one, and types are something that comes without a justification. Anyway, the idea is, if you have a language, you can think of source code written in the language as a giant lambda term, where you have all lambdas upfront and only composition in the body. A tree of symbols to be composed, essentially. And then to interpret this source code in a language, you supply definitions of the language's primitives as arguments to the source code term. Now if your language is typed, the primitives need to be chosen in such a way, so that the interpreted term (the source code applied to language primitives) fails to normalize if the program is not typed correctly. You can then have a correspondence between the primitives of the typed language that typecheck and simpler set of primitives of the same language used purely for computation, used under the assumption that the program typechecks. This correspondence "defines" the typing mechanism of your language (in untyped lambda terms).
- tromp 1y ago
  > have all lambdas upfront and only composition in the body That is only possible for a very limited subset of lambda terms. For example, it's not possible for the one-point basis A = λx λy λz. x z (y (λw. z)) from which any closed lambda term can be constructed by composition.
  - js8 1y ago
    Yes, that's deliberate though. (I will call these "concrete" terms, because they lack abstraction in the body, but I am looking for a good name. In fact, no universal one-point basis can be expressed as a single term like that, you need a composition of two; the concrete property is not preserved in composition, although it might be preserved in weaker bases than S,K, such as B,C,K - kind of affine logic.) Anyway, the reason I am interested in concrete terms is I want to define typing judgements in ULC somehow. (In CoC, all mathematical questions can be rephrased as is there an object of given type T, and you need to be able to formalize questions somehow to formalize metamathematics.) An obvious definition of typing judgement in ULC would be: term x is of type B in a typed language A (both A and B are given terms) iff there exists a term x that satisfies Ax = B (the equality is judgemental after beta-normalization). However, this definition doesn't work, because a general term x can just disregard A and return B directly. But - I think if we restrict x to be a concrete term in the above definition (possibly with a given number of upfront lambdas - not sure if that is required), then I think we can make the definition to work. I also suspect concrete terms can be sort of "deconstructed from the outside". In general, we cannot resolve equality of terms, but I suspect that concrete terms can be analyzed (and quoted) within ULC. One thing I realized about your CoC implementation - I think you embed CoC into ULC in an indirect way, working with CoC terms in a quoted way. And that's fine, but what I want is to have CoC in ULC directly, i.e. have a base set of ULC terms for the primitives of CoC language. But that also can be thought of as the CoC interpreter being restricted to apply on concrete terms, giving them meaning by substituting the base inside. In other words, concrete terms are kind of "inside view" of quoting. (Maybe we should call them "data terms", because they effectively carry only data and no executable payload.) Having the concept of concrete terms in the ULC metalanguage can also help to define interaction to the external world, that you only accept data not executables, something that you kinda do through the "monadic" interface. (You need to "remember" that a term only accepts quoted data, it cannot be made explicit in ULC language. The advantage of concrete terms is they are independent on your choice of quoting operator.) Anyway, I am not sure if I am making sense, I am trying to grapple with this myself, so it's OK if you don't think concrete terms are a useful concept.
jonathanstrange 1y ago
The typed lambda calculus is not Turing complete.
- js8 1y ago
  Not quite true, depends on the flavor of the type system you use. Church's simply typed is not, but other type systems are. I think one way to make it Turing complete is to add typing rule for Y combinator as an axiom to your simple type system, but I am not sure.
  - jonathanstrange 1y ago
    Yes, I had Church's simply typed lambda calculus in mind. You need to add a fix point combinator or general recursion.

tromp 1y ago

I implemented the Calculus of Constructions in untyped lambda calculus in order to shorten the 643 byte C program computing Loader's Number to 1850 bits (under 232 bytes) [1], as one of the milestones reached by my functional busy beaver function [2]. [1] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634 https://codegolf.stackexchange.com/questions/176966/golf-a-n... [2] https://oeis.org/A333479 https://oeis.org/A333479

js8 1y ago
I think this is great. I think you should write a paper on it. I suspect it might need some kind of commutative diagram proof, i.e. if you express things in CoC formalized within BLC you will get the same result as when you express in BLC formalized within CoC, I am not sure from the top of my head. (Kind of similar to showing that self-interpreting quoted interpreter on quoted program is the same as quoting the result of running the interpreter on the program.) And of course, this proof of equivalence should have formalization both in CoC (Lean?) and BLC. My hope is eventually someone writing a book on logic where the metalogic will be just untyped lambda calculus. Proofs will be just beta-reduction and judgemental equality. And everything will be in the form, let's study properties of these lambda terms that I came up with (the terms will of course represent some other logic such as CoC, simply typed LC, or even LC itself etc.).

CaptainOfCoit 1y ago

> And we should aim for that, the babel tower of languages doesn't really help anyone. What exactly do you mean with this? That the amount of programming languages available isn't actually helpful, it's detrimental?

Mountain_Skies 1y ago
Everyone should be free to unite behind my choices. It's obviously what is best for everyone.
- js8 1y ago
  That's a rather cheap retort. I am not saying everybody should use raw untyped lambda calculus for their programming, just that we would all benefit if we could translate languages we use to and from it, because then we could interoperate with any other code, refactor it, etc.
  - actionfromafar 1y ago
    Isn’t structure lost in the compilation process? I mean, we already have bits and pieces of what you want, like an assembler to C decompiler, but the output isn’t very nice without the types. And how many languages can run on the CIL in dotnet. Say we create a CIL to lambda calculus compiler. Where do we go from there?
    - js8 1y ago
      A CIL to LC compiler is effectively an emulator of CIL in LC. That is, every primitive of CIL has a corresponding LC term, which operates on the CIL execution state. So then you can express functions from .NET standard library as terms in LC. Now let's say you do the same for JVM. Now you can start looking at all these lambda terms and search for some similarities. For example, you might notice that some list functions are equivalent if you transform the representation in a certain invertible way. This gives you a way to express functions from one standard library in the other. In general, I think we should try to translate wide variety of human programs into lambda calculus and then try to refactor/transform the lambda terms to spot the common patterns.

entaloneralie 1y ago

A lot of languages(including forth) maps really poorly to LC. Read some of the Forth writing on portability at all costs: http://www.ultratechnology.com/antiansi.htm http://www.ultratechnology.com/antiansi.htm

tromp 1y ago
Simple pure concatenative languages map quite well though [1]. [1] https://github.com/tromp/AIT/blob/master/ait/mlatu.lam https://github.com/tromp/AIT/blob/master/ait/mlatu.lam
- entaloneralie 1y ago
  Joy, right? Not Forth. Conversion between spagetti stacks and pure stack programming(in which the stack contains numbers and no GC) has a massive translation cost if you go from LC to Forth and back.
  - js8 1y ago
    Forth is an imperative language and as such you will have to model memory state (at least) somehow, if you want to use purely functional language as a representation. But that's the cost of doing business. The thing is though, you don't translate to LC for performance, but for understanding. At any point, the LC evaluator might recognize a known subterm and replace it with a known equivalent. Depending on the goal, that might help to improve evaluation performance (skip known steps of beta reduction), reduce memory consumption (reduce size of the term), or improve readability (refactor code to use better known abstractions).
skybrian 1y ago
It's difficult to understand what they were actually doing, but reading between the lines, it sounds like an advantage of 'machine Forth' is writing some Forth words in assembly? I can see why that would run much faster for a jpeg decoder.

lambdaone 1y ago

Grounding programming languages in mathematics like this is essentially the goal of Strachey and Scott's denotational semantics, which has been very influential in programming language theory: https://en.wikipedia.org/wiki/Denotational_semantics https://en.wikipedia.org/wiki/Denotational_semantics

bananaflag 1y ago
All approaches to semantics of programming languages are mathematical, the denotational one is not "more mathematical" than the rest.
js8 1y ago
Not really a big fan, because the formalization of DS always left something desired, but I think a big difference with formalization in ULC is that ULC is (mostly) materialist while DS is structuralist. So the initial formalization into ULC can be automated - if you have semantics of your language already implemented as an interpreter in another language, you can use this as a starting point. With DS - I am not sure. I feel most people who build new languages don't provide DS specification.

deleted 1y ago

[deleted]

mighmi 1y ago

It's a real cool idea to compile everything down to lambda calculus and then you solve all semantics issues. (If something fits) you can convert 1:1, use general libraries in one language in others without loss etc. Ah, what a beautiful world it could be!