3 ms·
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
by awesomeMilou 3y ago
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.
- chatmasta 3y agoIn 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-literal-types.html https://www.typescriptlang.org/docs/handbook/2/template-lite...
- prologist 3y agoAny sufficiently advanced type system is indistinguishable from Prolog.
- baq 3y agoNote 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=lpn-htmlse5 https://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=...
- divs1210 3y agocommenting for future reference. that's a great quote.
- prologist 3y agoThanks. 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 https://shenlanguage.org/OSM/Recursive.html
- divs1210 3y agoYes! I have played with Shen before. IIRC the type checker is literally a Prolog.