I have this blog post idea kicking around in my head, which seems totally inadvisable but which I’m probably going to waste months of my life on at some point. It goes something like…

It seems decently well known that you can simulate dependent types with GADTs and higher-kinded types. I’m pretty sure that object algebras let you simulate GADTs, or at least certain aspects of them. I don’t really understand the GADTs-as-dependent-types things well, so I don’t know whether it requires something extra (like existential types), but those can be encoded as well. And brands allow you to shoehorn higher-kinded types into TypeScript.

Do you see where I’m going with this