Chapter 6. Programming with first-class types

In Idris, as you’ve seen several times now, types can be manipulated just like any other language construct. For example, they can be stored in variables, passed to functions, or constructed by functions. Furthermore, because they’re truly first-class, expressions can compute types, and types can also take any expression as an argument. You’ve seen several uses of this concept in practice, in particular the ability to store additional information about data in its type, such as the length of a vector.

In this chapter, we’ll explore more ways of taking advantage of the first-class nature of types. You’ll see how type-level functions can be used to give alternative names to types and also to calculate the type of a function from some other data. In particular, you’ll see how you can write a type-safe formatted output function, printf. For printf, the type (and even number) of arguments to the function are calculated from a format string provided as its first argument. This technique, calculating the type of some data (in this case, the arguments to printf) based on some other data (in this case, the format string) is often useful. Here are a couple of examples:

6.1. Type-level functions: calculating types

6.1.1. Type synonyms: giving informative names to complex types

6.1.2. Type-level functions with pattern matching

6.1.3. Using case expressions in types

6.2. Defining functions with variable numbers of arguments

6.2.1. An addition function

6.2.2. Formatted output: a type-safe printf function

6.3. Enhancing the interactive data store with schemas

6.3.1. Refining the DataStore type

6.3.2. Using a record for the DataStore

6.3.3. Correcting compilation errors using holes

6.3.4. Displaying entries in the store

6.3.5. Parsing entries according to the schema

6.3.6. Updating the schema

6.3.7. Sequencing expressions with Maybe using do notation

6.4. Summary