O'Reilly logo

Seven More Languages in Seven Weeks by Bruce Tate, Jack Moffitt, Frederic Daoud, Ian Dees

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required