Hacker News Reader

Comment by quickthrower2 | Hacker News Reader

Please tell me this means you can do dependent types! I have no idea how this works, seems like magic and seems like anything is possible.

Maybe "dependent-but-stringly typed" is possible?

View on HN

TypeScript has a very limited form of dependent typing made available through `typeof`, but it does not have dependent typing as e.g. Idris does. However, in general, these sorts of demonstrations do nothing to show that a language can be dependently typed. These sorts of demonstrations show that a type system is Turing complete. However, a type system can be Turing complete without being dependent. For example, type-level integers might be completely different from run-time integers with no way to things from the latter to the former.

Sure, but plenty of type systems are Turing complete. What makes this demo impressive is the (unique?) feature of string literal types and template literal types, which lets you operate on text (like, actual text, with no weird type-level encodings).

Well, certainly string literal types have been around in GHC Haskell for quite a while (7.10.x). They've also been a thing in Scala 2.12.x although the 'implementation' was some sort of weird type checker 'hack'. I believe Scala 3 supports them natively.

I can't speak to the ergonomics of actually implementing anything which uses them internally since I've never really had much use for them outside using the surface-level API of a couple of libraries.

Reply on news.ycombinator.com