Type-Driven Development with Idris

Chapter 7. Interfaces: using constrained generic types

This chapter covers

• Constraining generic types using interfaces
• Implementing interfaces for specific contexts
• Using interfaces defined in the Prelude

In chapter 2, you saw that generic function types with type variables could be constrained so that the variables stood for a more limited set of types. For example, you saw the following function for doubling a number in any numeric type:

double : Num a => a -> a
double x = x + x

The type of double includes a constraint, Num a, which states that a can only stand for numeric types. Therefore, you can use double with Int, Nat, Integer, or any other numeric type, but if you try to use it with a non-numeric type, such as Bool, Idris will report ...