Wrapping Up Idris
If you’re used to dynamically typed languages, Idris represents a tremendously steep technical challenge. If, on the other hand, you’re already comfortable with dependent types and category theory, you’ll likely appreciate the many advances that Edwin Brady has made to bring this language closer to the mainstream. Let’s break down the strengths and weaknesses.
Strengths
With Idris, types know more, so they can do more. In this chapter, we looked at four practical improvements due to dependent types:
-
With more type information, compilers can catch more complex bugs, including logic errors, at compile time.
-
When types can express structure, automatic code completion can go far beyond basic syntax—to a degree that’s potentially ...
Get Seven More Languages in Seven Weeks now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
