I'm always curious what people are using the more exotic type system functionality of e.g. Haskell or Idris for in practice. It was interesting to hear that even Simon didn't expect such things to be used in industry quite yet.
Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program.
Further to that point, the most complex programs I can think of (perhaps you may be able to offer other opinions, which I welcome) are AAA game engines. What are the reasons why the big engines out there are not using higher-kinded types, dependent types and the like? Is this just because of pragmatic issues such as the languages the developers learned in school not supporting these features, or because here-to-date functional languages supporting these features lacked the appropriate throughput of C/C++, where one can layout data for cache-efficiency?
Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program.
Further to that point, the most complex programs I can think of (perhaps you may be able to offer other opinions, which I welcome) are AAA game engines. What are the reasons why the big engines out there are not using higher-kinded types, dependent types and the like? Is this just because of pragmatic issues such as the languages the developers learned in school not supporting these features, or because here-to-date functional languages supporting these features lacked the appropriate throughput of C/C++, where one can layout data for cache-efficiency?