Seven More Languages in Seven Weeks

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