Seven More Languages in Seven Weeks

Day 3: Dependent Types in Action

In Day 2, you built some dependent data types, including vectors and a leap year. You may have noticed that these types took more up-front work than before. What features could possibly make all that extra effort worthwhile? Settle in. We’re on the case.

First, we’ll look at the spectacular ways the type system can help you write programs. With more information, Idris can take code completion places you’ve likely never been before. Then, we’ll look at using the type system to reason about the way our programs behave by constructing a proof. Finally, we’ll see how reasoning in Idris can help us improve our programs in other languages. It’s a busy day, so let’s get started.

Smarter Completion

In this section, we’re ...