🎥 f(by) 2020: Dependent types is a surprisingly good talk from None 🇷🇺 about dependant types in Haskell an Idris. It starts from quite good examples what dependent types are about and ends with a research on their state and future in the industry. This is the first talk I’ve watched so far that talks not only about how fun “typing on steroids” but also how practical it is.
We have discovered that it [a real-world application with dependent types] can be done, and it brings significant value, but also a high cost.
🤷♀️