A taste of dependent types with Idris

If you aren't familiar with Haskell's syntax I've included this section explaining the fundamentals of Idris syntax, otherwise you can skip this part.

fortyTwo : Nat
fortyTwo = 42

numberList : List Nat
numberList = [1, 2, 3]

myBoolean : Bool
myBoolean = False

theString : Type
theString = String

addOne : Nat -> Nat
addOne n = n + 1

addOne 10 -- 11
addOne 0 -- 1

plus : Nat -> Nat -> Nat
plus a b = a + b

plus 10 7 -- 17
4 `plus` 8 -- 12

multiply : Nat -> Nat -> Nat
multiply = \a, b => a * b

multiply 4 3 -- 12
10 `multiply` 3 -- 30

data Fruit = Apple | Orange | Pear | Banana

orange : Fruit
orange = Orange

data Pair a b = MkPair a b

myTuple : Pair Nat String
myTuple = MkPair 10 "test"

otherTuple : Pair Bool Fruit
otherTuple = MkPair False Pear

data Maybe a = Nothing | Just a

perhapsCarModel : Maybe String
perhapsCarModel = Just "Fiat"

largestNumber : Maybe Nat
largestNumber = Nothing

-- equivalent GADT definition for the Maybe type
data Maybe : Type -> Type where
  Nothing : Maybe a
  Just : a -> Maybe a

data Maybe : Type -> Type where
  Nothing : Maybe a
  Just : a -> Maybe a

maybe : (a -> b) -> b -> Maybe a -> b
maybe fun fallback val =
  case val of
    Nothing => fallback
    Just x => fun x

data List : Type -> Type where
  Nil : List a
  (::) : a -> List a -> List a

map : (a -> b) -> List a -> List b
map fun list = case list of
    Nil => Nil
    (x::xs) => f x :: map fun xs

-- equivalent definition of map with syntax sugar
map : (a -> b) -> List a -> List b
map _ [] = []
map f (x::xs) = f x :: map f xs

One of the core features of Idris is what we call type driven development. By leveraging its type system we can get a lot of help from the compiler when implementing functions. Writing a program in Idris can be seen as a conversation between the programmer and the compiler. We start by giving a type definition for some function, then we define the function and then refine the function until we have an implementation that type checks. Hopefully in the end we have a program that works. This process is much helped by dependent types since we can be very precise about our functions type and express dependent properties otherwise not possible in most languages.

filter : (a -> Bool) -> List a -> List a
filter p l = ?filter_rhs

-- REPL output
Main> :t filter_rhs
 0 a : Type
   l : List a
   p : a -> Bool
-------------------------------------
hole : List a

Let's say we want to implement the filter function. We start by giving its type and a function definition which introduces the function arguments on the LHS. On the right we put a typed hole called filter_rhs. When we load the code into the Idris REPL and check the type of the hole we get the output above listing everything we have access to in scope.³ We see that we have access to the predicate p and the list l.^{4 5}

filter : (a -> Bool) -> List a -> List a
filter p [] = ?filter_rhs_1
filter p (first :: rest) = ?filter_rhs_2

-- REPL output
Main> :t filter_rhs_1
 0 a : Type
   p : a -> Bool
-------------------------------------
hole : List a

Main> :t filter_rhs_2
 0 a : Type
   p : a -> Bool
   first : a
   rest : List a
--------------------------------------
filter_rhs_2 : List a

Using an interactive editor we can now case split on l to pattern match on all the data constructors of the List type. Now we have two holes, one for each list constructor. For the empty case we don't have much to work with. We have the predicate p, but no elements of type a to apply it to. Here we can actually ask the compiler to search for a solution for us. In this case there is only one valid solution which is to return the empty list. For the cons constructor :: we have more to work with. We have a value first of type a which we can pass as an argument to p so that we get back a Bool. Since we want to filter out elements which don't match the predicate we have to return different things depending on the result of p first, therefore we can use an if expression.

filter : (a -> Bool) -> List a -> List a
filter p [] = []
filter p (first :: rest) = if p first then first :: filter p rest else filter p rest

For the case where we want to keep first as part of the list we put it at the front of the list and make a recursive call to filter with the remaining part of the list to be filtered, rest. If the predicate doesn't hold then we must discard first and so we just make a recursive call to filter with the rest, ignoring first.

Using this pattern of type, define, refine is very beneficial when developing in Idris. By leaning on Idris' type system it can guide you towards the correct implementation and the more information about your functions you can encode in your types the higher the chances are that you end up with the correct implementation. However, Idris' case split and search isn't fool proof and doesn't absolve you as a developer from thinking about the implementation, but the compiler can certainly help you along the way.

A dependent type is a type whose definition depends on a value. A language which supports dependent types supports first class types. In such languages types are just regular values like any other value. There is no distinction between the type level and the term level. In practice this means that you can assign names to types, functions can take types as arguments and return types. In other words you can compute types.

stringOrNat : (isStr : Bool) -> Type
stringOrNat True = String
stringOrNat False = Nat

Here we have an example of a function which returns a type depending on the input boolean which we have named isStr in the type although it's not strictly necessary to give it a name in this case. What's the point of defining functions which computer types if not to use it as part of some other type.

lengthOrDouble : (isStr : Bool) -> stringOrNat isStr -> Nat
lengthOrDouble True str = length str
lengthOrDouble False num = num + num

Here we introduce our first dependent function. lengthOrDouble's first argument is a value isStr of type Bool, however the second arguments type is dependent on the value of isStr since we are using the previously defined stringOrNat to compute the type. If isStr is True then the second argument is a String and so str is a value of type String and we can return the length. Otherwise, it's a Nat and we return the double of that value num. We can now test this in the REPL by passing a Bool to lengthOrDouble.

-- REPL output
Main> :t lengthOrDouble True
lengthOrDouble True : String -> Nat

Main> :t lengthOrDouble False
lengthOrDouble False : Nat -> Nat

Main> lengthOrDouble True "hello"
5 : Nat

Main> lengthOrDouble False 20
40 : Nat

Notice how the type changes depending on the value of the Bool passed to lengthOrDouble.

However, this example is quite contrived so what sort of useful things can we do with dependent functions? If you've ever programmed in C you will be familiar with the function printf which formats a string. This is in fact a dependent function! printf takes an argument string with placeholders for strings and numbers such as '%s' and '%d' then takes those string and numbers as arguments and returns a string where the placeholders are replaced with the values. So the type of the function depends on what sort of string it is given. In most languages printf is implemented in an unsafe manner. If you supply values that don't match the placeholders in the string your program will crash with a runtime error, but in Idris we can implement a type safe version of printf.

-- REPL output
Main> :t printf "Hello my name is %s and I'm %d years old"
printf "Hello my name is %s and I'm %d years old" : String -> Nat -> String

Main> :t printf "Hello my name is %s and my friend here is %s"
printf "Hello my name is %s and my friend is here is %s" : String -> String -> String

Main> printf "Hello my name is %s and I'm %d years old" "Bob" 17
"Hello my name is Bob and I'm 17 years old" "Bob" : String

Main> printf "Hello my name is %s and I'm %d years old" "Bob" "woops"
builtin : Type mismatch between
          String (Type of "woops")
and
          Nat (Expected type)

The implementation is slightly more involved than the previous example, but the principle is exactly the same. If you want to take a look at the source code you can find it here.

Lets take a look at implementing append for the List type.

append : List a -> List a -> List a
append xs ys = ?append_rhs

We start by case splitting on the first argument xs.

append : List a -> List a -> List a
append [] ys = ?append_rhs_1
append (first :: rest) ys = ?append_rhs_2

For the first case where xs is empty there really isn't much we can do other than return the second list ys and indeed the compiler could figure this out for you when searching for a solution. However, the second case is slightly more interesting.

Here we have to think a bit about what we want because there are several solutions which would type check. What we want is to traverse over the entire list xs and then add the list ys to the end. Unfortunately if we had left it to the compiler to search for a solution it would have returned ys, which would type check because ys is of type List a as well, but isn't the behaviour we're looking for.

append : List a -> List a -> List a
append [] ys = []
append (first :: rest) ys = ys -- woops, wrong implementation

Luckily for us there is a solution to this problem. If we can give the compiler more information about the List type we're working on perhaps it could infer the correct solution.

data Nat : Type where
  Z : Nat        -- zero
  S : Nat -> Nat -- successor of a natural number

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a                       -- the empty vector
  (::) : a -> Vect k a -> Vect (S k) a -- adding an element to the front of a vector

Here we introduce the Vect type which is just like the List type, but also parameterised over the length of the list. We're using the Nat type for natural numbers here to represent the length which itself has a recursive definition as shown above. However, Idris includes syntax sugar for this type as well, so we can write 3 instead of S (S (S Z)) for example. In this case Nil, representing the empty vector, takes no arguments and gives us a list of type Vect Z a which is a list of length zero.

For the cons constructor :: we take some element of type a and vector of type Vect k a where k is the length and return a vector of type Vect (S k) a . Since we're adding one element to the front of the vector it will have the length S k otherwise known as k + 1.

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

Since we are now defining append on Vect we can encode an invariant in the type signature. The resulting vector we get from appending two vectors of length n and m is always going to be of length n + m.

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ?append_rhs_1
append (first :: rest) ys = ?append_rhs_2

Again we start by case splitting on the first list xs.

-- REPL output
Main> :t append_rhs_1
 0 m : Nat
 0 a : Type
   ys : Vect m a
 0 n : Nat
-------------------------------------
append_rhs_1 : Vect m a

Inspecting the first typed hole we find that append_rhs_1 has the type Vect m a which happens to be the type of ys here. Since this is the only value which matches the type we must return it (again the compiler could infer this for us), but the original return type we declared for append had the length n + m how come it has changed? Since we pattern matched on the first list xs with the empty case Nil / [] here the compiler has inferred the type of n to be Z / 0 which is the type of the Nil constructor as we defined it in our Vect type. Therefore, the return type of append_rhs_1 has changed to Vect (0 + m) a in this case and the compiler has simplified this to the normal form Vect m a. By pattern matching on the first list xs we've learned more about the type which lets the compiler make more inferences.

-- REPL output
Main> :t append_rhs_2
 0 m : Nat
 0 a : Type
   first : a
   rest : Vect len a
   ys : Vect m a
 0 n : Nat
-------------------------------------
append_rhs_2 : Vect (S (len + m)) a

In the second case where xs contains elements the typed hole is of a different type. Here we have to return a Vect of length S (len + m) where len is the length of rest and m is the length of ys. We can do this by using :: to construct a vector where first is the head and the tail is the result of calling append on rest and ys. Let's check that the lengths match.

||| Taken from append_rhs_2:
||| first : a
||| rest : Vect len a
||| ys : Vect m a

first :: ... -- Vect (S ?something) a

append rest ys -- Vect (len + m) a

first :: append rest ys -- Vect (S (len + m)) a

-- Vect
append rest ys

• Adding first to the front of some list will give use a vector of length S ?something where ?something is the length of the vector that first is being added to as given by the :: definition in the Vect type we defined.
• The length of append rest ys is len + m as given by our definition of append.

Therefore, it follows that the length of first :: append rest ys will be S (len + m) which is exactly what we were looking for!

There is really only one way of implementing this function therefore we can let the compiler search for a solution and it will give us the correct answer.

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (first :: rest) ys = first :: append rest ys

As we've seen providing more information about the type in the data structure can be useful and there are several reasons for that.

• it gives us more information about the type which we can exploit depending on the context

• it lets us encode invariants in functions that manipulate dependent data structures

  • these invariants make our code more type safe by reducing the total amount of valid implementations meaning implementations that pass the type checker

However, this doesn't mean you always want to add all the extra type information you possibly can to any given data structure. Once you become more expressive about your types and the type grows more complex you may find it harder to implement functions which manipulating said data structure. The more types you carry around and invariants in your functions or data structures the more things the compiler needs to be able to prove about your functions so that the program type checks and for more complex propositions this requires you to provide proofs in your functions so that the compiler may resolve the types.

Dependent types allow us to express propositions as types. This is useful because if we can show that these propositions hold true then we have proven the validity of said proposition in the mathematical sense. The direct relationship between formal proofs and computer programs is knows as the Curry-Howard equivalence. Historically it has also been the main use of dependent types in theorem provers such as Coq and Agda.

So how do we write proofs in Idris? We start by describing propositional equality between types as its own type. Let's start by defining one such data type for propositional equality between natural numbers.

data EqNat : Nat -> Nat -> Type where
  SameNat : (num : Nat) -> EqNat num num

Here we define a data type EqNat which takes two Nat's and gives us back a Type. It has one constructor SameNat which takes only one argument the value we call num of type Nat and returns a type of EqNat num num. Thereby enforcing that the two Nat values in the type are indeed the same number. Now we can start off with a simple proof of equality.

smallProofEq : EqNat (2 + 2) 4
smallProofEq = ?foo

Let's try to prove that 2 + 2 = 4, we start by checking the typed hole.

Main> :t foo
-------------------------------------
foo : EqNat 4 4

Here we see that the compiler has already simplified 2 + 2 for us. So the return type has now changed to EqNat 4 4. So how do we provide a value of type EqNat 4 4? Well EqNat only has one constructor so lets start with that.

smallProofEq : EqNat (2 + 2) 4
smallProofEq = SameNat ?foo

-- REPL output
Main> :t foo
-------------------------------------
foo : Nat

We now see that ?foo has the type Nat so we can now pass 4 to the SameNat constructor.

smallProofEq : EqNat (2 + 2) 4
smallProofEq = SameNat 4

Now we have a proof that 2 + 2 = 4, but what happens if we try to prove something that isn't true?

smallProofNotEq : EqNat (2 + 2) 5
smallProofNotEq = SameNat 4

When checking right-hand side of smallProofNotEq with expected type
        EqNat (2 + 2) 5
     
Type mismatch between
        EqNat num num (Type of SameNat num)
and
        EqNat 4 5 (Expected type)

Specifically:
        Type mismatch between
                0
        and
                1

Here we get a type error complaining that the compiler can't unify 0 with 1. Remember that the definition of Nat is recursive so the compiler has tried to reduce both numbers down to zero, but fails because 5 is greater than 4, therefore we get the type error that 1 is not equal to 0.

smallProofNotEq : EqNat (2 + 2) 5
smallProofNotEq = smallProofNotEq

smallProofNotEq is possibly not total due to recursive path smallProofNotEq

successorEq : EqNat x y -> EqNat (S x) (S y)
successorEq p = ?successorEq_rhs

successorEq : EqNat x y -> EqNat (S x) (S y)
successorEq (SameNat n) = ?successorEq_rhs

-- REPL output
Main> :t successorEq_rhs
  n : Nat
------------------------------------------
successorEq_rhs : EqNat (S n) (S n)

successorEq : EqNat x y -> EqNat (S x) (S y)
successorEq (SameNat n) = SameNat (S n)

-- Repl output
Main> :total successorEq
successorEq is Total

Main> successorEq (SameNat 10)
SameNat 11 : EqNat 11 11

Main> successorEq (SameNat 4)
SameNat 5 : EqNat 5 5

data (=) : a -> b -> Type where
  Refl : x = x

smallProof : 2 + 2 = 4
smallProof = Refl

successor : (x = y) -> S x = S y
successor Refl = Refl

-- REPL output
Main> the (1 = 1) Refl
Refl : 1 = 1

Main> the (7 = 7) Refl
Refl : 7 = 7

Main> successor (the (1 = 1) Refl)
Refl : 2 = 2

Main> successor (the (7 = 7) Refl)
Refl : 8 = 8

tryZip : Vect n a -> Vect m b -> Maybe (Vect n (a, b))

tryZip : Vect n a -> Vect m b -> Maybe (Vect n (a, b))
tryZip xs ys = if length xs == length ys then Just ?help else Nothing

Main> :t help
 0 b : Type
 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
help : Vect n (a, b)

checkEqNat : (n, m : Nat) -> Maybe (n = m)
checkEqNat Z Z = Just Refl
checkEqNat (S k) Z = Nothing
checkEqNat Z (S j) = Nothing
checkEqNat (S k) (S j) =
  case checkEqNat k j of
    Nothing => Nothing
    (Just Refl) => Just Refl

checkEqNat (S k) (S j) =
  case checkEqNat k j of
    Nothing => Nothing
    (Just (Refl {x = k}) => Just (Refl {x = S k})

tryZip : Vect n a -> Vect m b -> Maybe (Vect n (a, b))
tryZip xs ys = ?tryZip_rhs

Main> :t tryZip_rhs
 0 b : Type
 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
tryZip_rhs : Maybe (Vect n (a, b))

tryZip : {n, m : Nat} -> Vect n a -> Vect m b -> Maybe (Vect n (a, b))
tryZip {n} {m} xs ys = ?tryZip_rhs

Main> :t tryZip_rhs
 0 b : Type
 0 a : Type
   n : Nat
   m : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
tryZip_rhs : Maybe (Vect n (a, b))

tryZip : {n, m : Nat} -> Vect n a -> Vect m b -> Maybe (Vect n (a, b))
tryZip {n} {m} xs ys =
  case checkEqNat n m of
    Nothing => Nothing
    (Just Refl) => ?hole

Main> :t hole
 0 b : Type
 0 a : Type
   n : Nat
   ys : Vect n b
   xs : Vect n a
   m : Nat
-------------------------------------
hole : Maybe (Vect n (a, b))

tryZip : {n, m : Nat} -> Vect n a -> Vect m b -> Maybe (Vect n (a, b))
tryZip {n} {m} xs ys =
  case checkEqNat n m of
    Nothing => Nothing
    (Just Refl) => Just (zip xs ys)

Main> tryZip [1, 2, 3] [4, 5, 6]
Just [(1, 4), (2, 5), (3, 6)]

Main> tryZip [True, False] [False, False]
Just [(True, False), (False, False)]

Main> tryZip ["hello"] ["nada", "adios"]
Nothing

Main> tryZip ['a', 'b', 'c'] ['d']
Nothing

• Idris homepage
• Type-Driven Development with Idris
• Propositions as Types by Philip Wadler at StrangeLoop (2015)
• Software foundations book in Idris
• Edwin Brady's four part video series on dependent types in Idris