In general I am torn between the enthusiasm people like the author bring to the table and their apparent lack of due diligence regarding a discipline that has been subject to thorough research for decades.
So, I'm the author and I'm aware there are smarter people than me working on things like this, but my question is mostly whether there's a threshold where things can be useful. As an honest question, in C++ I think there's a "stack limit" of like 15 deep for generic types to avoid the fact that the types are Turing complete. Is there something that can be done that addles the type system but makes useful things possible? I think that just because something isn't possible in the general case doesn't mean that the specific cases people are likely to encounter are impossible.
Of course there is a room for pragmatism when it comes to type system. Just lookup the computational complexity of HM inference. But to be useful, the restrictions need to be understood very well. Otherwise your implementation very probably ends up unsound.
https://cs.stackexchange.com/questions/12691/what-makes-type...
In general I am torn between the enthusiasm people like the author bring to the table and their apparent lack of due diligence regarding a discipline that has been subject to thorough research for decades.