Any sufficiently capable type system will make it possible to implement a form of functional programming.
These advanced type systems are essentially a form of pre-compile time scripting to assert certain guarantees about user defined types. It's the same mechanism that makes C++ templates turing complete.
In the case of TypeScript, most of the magic and crazy hacks are dependent on Template Literal Types [0], which is what allows inference based on arbitrary strings. Once you have that abstraction, you can just keep adding complexity to it.
Thanks. The Shen language takes this to its logical conclusion (pun intended) and implements a fully Turing complete type system. Types are specified with sequents which are essentially Prolog relations using a slightly different notation.[1]
Comments
Any sufficiently capable type system will make it possible to implement a form of functional programming.
These advanced type systems are essentially a form of pre-compile time scripting to assert certain guarantees about user defined types. It's the same mechanism that makes C++ templates turing complete.
In the case of TypeScript, most of the magic and crazy hacks are dependent on Template Literal Types [0], which is what allows inference based on arbitrary strings. Once you have that abstraction, you can just keep adding complexity to it.
[0] https://www.typescriptlang.org/docs/handbook/2/template-lite...
Any sufficiently advanced type system is indistinguishable from Prolog.
Note to readers: if the author’s username doesn’t make it obvious, it’s funny because is true.
If feeling adventurous, read e.g. https://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=...
commenting for future reference.
that's a great quote.
Thanks. The Shen language takes this to its logical conclusion (pun intended) and implements a fully Turing complete type system. Types are specified with sequents which are essentially Prolog relations using a slightly different notation.[1]
1: https://shenlanguage.org/OSM/Recursive.html
Yes! I have played with Shen before.
IIRC the type checker is literally a Prolog.