Comment by ajb
4 hours ago
TBH something like this sounds useful even without LLMs (although I haven't fully grokked this yet). The problem with the operational level is that you can't express the invariants etc at the type level - not least because you're working across multiple languages - so the kind of dumb issues that we're beginning to rule out at the level of the language at the process level still require lots of diligence in operational code. Some kind of shared "operational type system" that could be integrated into relevant languages would potentially help a lot.
Shen has some really unique properties that are under-developed here. It's type system itself is Turing complete and very flexible / expressive. Also, the Shen kernel is extremely compact, and easy to port into a wide variety of runtime languages (C, Lisp, Ruby, Python, JS, Go, etc https://news.ycombinator.com/item?id=39602472
I didn't focus a ton on Shen in the blog post, because the underlying principles aren't really about the implementation. Shen is very cool tho.
> It's type system itself is Turing complete
That's not a good thing! A Turing complete type system means that compilation is potentially undecidable and non-terminating. The whole unintuitive mess in dependently-typed systems about "definitional" equality (loosely speaking, a notion of equalities that are 'trivially' checked as part of evaluation) is entirely about avoiding Turing-complete type checking!
I mean yes, that's a risk, and you are correct. In practice, is your spec about the shape of the app you want to build really going to be that complicated?
But I mentioned its Turing completeness as a lazy shorthand to illustrate that it is far more flexible and expressive than what people think of as a "type system". https://shenlanguage.org/OSM/Recursive.html