[throw_await]

Typescript has something that can be used as dependent types, but it wasn't intended as a language feature, so the Syntax is not as ergonomic as Agda: https://www.hacklewayne.com/dependent-types-in-typescript-se...

[codethief]

That whole blog is one big and fascinating rabbit hole into type theory! Thanks for the link!