Sexy Types ΓÇô Are We Done Yet?

Опубликовано 17 августа 2016, 1:38

Functional programming languages have been a very productive laboratory for developing new language features and in particular powerful type systems. The use of static typing represents the most widespread and successful application of formal verification. Many of the innovations in research languages like Haskell can traced to new features in mainstream programming languages like C#. What will be the new wave of innovations in types that will appear in mainstream languages? Exciting candidates include features like dependent types and linear types and special support for security. Or have we now reached a fix point in the development of type systems? Are some of the latest developments in the type systems of languages like Haskell, Scala and Agda also candidates for adoption by mainstream languages? Have the most recent developments in type systems attained a level of complexity that puts them out of the reach of mainstream programmers?