3 ms·

My understanding is that you control evaluation more explicitly in concatenative combinators. Combinatory logic cannot destructure programs, only apply them. I

• tromp 3y ago
  A typed combinatory logic is introduced in [1]. [1] https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theory_2016/handout_7.pdf https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theo...
  • js8 3y ago
    Yes, you can do that, but then you can express only well-typed programs in that logic. My point is, I believe, that concatenative language such as Joy doesn't prescribe a specific way to do the evaluation (or type-checking) and as such is less restrictive (or perhaps just different) than combinatory logic. This is despite the fact that they are both Turing-complete in the sense they can emulate each other (there is a subset of combinatory logic programs that correspond to concatenative language and vice versa). I don't want to hammer on the other analogy, but perhaps your question (why not just use combinatory logic) is kind of like asking why don't we only use natural numbers, if they are set-theoretically equivalent with integers at large, and at the same time a smaller set. The reason is, of course, the integers reveal something about the structure of natural numbers (or do they artificially add this structure, which one is it, really?). I think concatenative combinators can be considered analogous to integers here.