Looks very interesting. I played around with (dependently) typed combinatory logic a while ago, using a system called "illative combinatory logic" http://www.chriswarbo.net/blog/2012-12-01-typed_combinators.... and I agree that's it's hard to actually use ;)
I was approaching typed combinator expressions as a target for AI systems (this predated transformers; I was thinking more like genetic programming, inductive programming, etc.), but in order to trust the results it would need to be free from paradoxes (like Type : Type).
Related: https://treecalcul.us
https://github.com/barry-jay-personal/tree-calculus/blob/mas...
TBH, I am not sure I understand how this is different from Tree Calculus. Is it just the addition of dependent types?
I wonder if combinators could be useful for neurosymbolic AI—either in the backward pass (e.g., training models on synthetic data) or the forward pass (e.g., iterative code generation with evolutionary algorithms). Combinators feel alien, making even Haskell or APL seem intuitive, but maybe that’s because they don’t align with human working memory. Language models, with their massive context windows, handle long-range dependencies in sequences well, even if their understanding is shallower in some ways. Could combinators, with their compositional and deductive nature, be a better fit for machines than humans? For example, instead of generating Python functions in an evolutionary approach[0], could we use combinators as the building blocks? They’re compact, formal, and inherently step-by-step, which might make them ideal for tasks requiring structured reasoning and generalization. What do you think?
[0]: https://jeremyberman.substack.com/p/how-i-got-a-record-536-o...
> I also cannot write this language, like I am not close to grokking it.
The hallmark of any good esoteric language. :)
I like those experiments: I did many experiments over christmas and some I will try to continue working on. It's just fun playing with pl theory and concrete implementations.
Dependent Types + Combinatory Logic is highly non-trivial, as is shown in this series of work by Altenkirch et al.:
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.F...
https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...
https://types2023.webs.upv.es/slides/S22/TYPES2023-Altenkirc...
I wonder: Where does rholang3 fit in this?