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 2: Getting Started With Dependent Types

Day 1 was about the basics, laying the foundation for today. Today, we’re going to take some of the mystery out of whether or not a program works. We’ll start with our type model.

Understanding Dependent Types

In most languages, types and values are independent. List, String, and Integer are types that describe the values [], "Hello", and 6. Said another way, types describe values.

In dependently typed languages like Idris, types still describe values, but types may also depend on values. This allows us to use more of the language to define our types.

For example, Idris has a vector family of types: Vect n a represents lists of length n and element type a. With most traditional type systems, you could ...

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