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 ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access