what's the deal with dependent types?
In this talk, I identify key ways in which dependently typed programming confounds our common expectations, and then transcends them. I expose language design issues where dependent types require a new deal. I hope to persuade you that this is not a big deal, and that it is a good deal. I discuss the impact of these issues on Epigram [3], the language designed by myself and James McKinna, and still evolving with help from Thorsten Altenkirch [1] and our colleagues in Nottingham and St Andrews.
dependent types epigram pattern matching