Looks very interesting. I played around with (dependently) typed combinatory logic a while ago, using a system called "illative combinatory logic" http://www.ch

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.html 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).