4 ms·
Sometimes I think I don't understand TypeScript's type system and then I see something like this and I realize I know even less than I thought
by hbn 3y ago
Sometimes I think I don't understand TypeScript's type system and then I see something like this and I realize I know even less than I thought
- awesomeMilou 3y agoAny 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.
- bazoom42 3y agoTypescript has conditional types, which means it can be used as a programming language itself. In theory you can write any arbitrary program - game of life is just an example. You have to define numbers and arithmetics from scratch though, so it is not very practical. Conditional types are probably rarely used in practial code, but it opens the door for a lot of geekery.
- ushakov 3y agoWe’re using conditional types for type inference in garph (https://garph.dev https://garph.dev)