Hacker News Reader

Comment by hbn | Hacker News Reader

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

View on HN

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.

Typescript 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.

We’re using conditional types for type inference in garph (https://garph.dev)

Reply on news.ycombinator.com