|
| 1 | +# Compile-Time Computations |
| 2 | + |
| 3 | +```idris |
| 4 | +module Tutorial.Dependent.Comptime |
| 5 | +
|
| 6 | +import Tutorial.Dependent.LengthIndexedLists |
| 7 | +
|
| 8 | +%default total |
| 9 | +``` |
| 10 | + |
| 11 | +In the last section - especially in some of the exercises - we started more and more to use compile time computations to describe the types of our functions and values. This is a very powerful concept, as it allows us to compute output types from input types. Here's an example: |
| 12 | + |
| 13 | +It is possible to concatenate two `List`s with the `(++)` operator. Surely, this should also be possible for `Vect`. But `Vect` is indexed by its length, so we have to reflect in the types exactly how the lengths of the inputs affect the lengths of the output. Here's how to do this: |
| 14 | + |
| 15 | +```idris |
| 16 | +(++) : Vect m a -> Vect n a -> Vect (m + n) a |
| 17 | +(++) [] ys = ys |
| 18 | +(++) (x :: xs) ys = x :: (xs ++ ys) |
| 19 | +``` |
| 20 | + |
| 21 | +Note, how we keep track of the lengths at the type-level, again ruling out certain common programming errors like inadvertently dropping some values. |
| 22 | + |
| 23 | +We can also use type-level computations as patterns on the input types. Here is an alternative type and implementation for `drop`, which you implemented in the exercises by using a `Fin n` argument: |
| 24 | + |
| 25 | +```idris |
| 26 | +drop' : (m : Nat) -> Vect (m + n) a -> Vect n a |
| 27 | +drop' 0 xs = xs |
| 28 | +drop' (S k) (_ :: xs) = drop' k xs |
| 29 | +``` |
| 30 | + |
| 31 | +Note that changing the order from `(m + n)` to `(n + m)` in the second parameter will cause an error at the second `xs`: |
| 32 | + |
| 33 | +```repl |
| 34 | +While processing right hand side of drop'. Can't solve constraint between: plus n 0 and n. |
| 35 | +``` |
| 36 | + |
| 37 | +You will learn why in the next section. |
| 38 | + |
| 39 | +## Limitations |
| 40 | + |
| 41 | +After all the examples and exercises in this section you might have come to the conclusion that we can use arbitrary expressions in the types and Idris will happily evaluate and unify all of them for us. |
| 42 | + |
| 43 | +I'm afraid that's not even close to the truth. The examples in this section were hand-picked because they are known to *just work*. The reason being, that there was always a direct link between our own pattern matches and the implementations of functions we used at compile time. |
| 44 | + |
| 45 | +For instance, here is the implementation of addition of natural numbers: |
| 46 | + |
| 47 | +```idris |
| 48 | +add : Nat -> Nat -> Nat |
| 49 | +add Z n = n |
| 50 | +add (S k) n = S $ add k n |
| 51 | +``` |
| 52 | + |
| 53 | +As you can see, `add` is implemented via a pattern match on its *first* argument, while the second argument is never inspected. Note, how this is exactly how `(++)` for `Vect` is implemented: There, we also pattern match on the first argument, returning the second unmodified in the `Nil` case, and prepending the head to the result of appending the tail in the *cons* case. Since there is a direct correspondence between the two pattern matches, it is possible for Idris to unify `0 + n` with `n` in the `Nil` case, and `(S k) + n` with `S (k + n)` in the *cons* case. |
| 54 | + |
| 55 | +Here is a simple example, where Idris will not longer be convinced without some help from us: |
| 56 | + |
| 57 | +```idris |
| 58 | +failing "Can't solve constraint" |
| 59 | + reverse : Vect n a -> Vect n a |
| 60 | + reverse [] = [] |
| 61 | + reverse (x :: xs) = reverse xs ++ [x] |
| 62 | +``` |
| 63 | + |
| 64 | +When we type-check the above, Idris will fail with the following error message: "Can't solve constraint between: plus n 1 and S n." Here's what's going on: From the pattern match on the left hand side, Idris knows that the length of the vector is `S n`, for some natural number `n` corresponding to the length of `xs`. The length of the vector on the right hand side is `n + 1`, according to the type of `(++)` and the lengths of `xs` and `[x]`. Overloaded operator `(+)` is implemented via function `Prelude.plus`, that's why Idris replaces `(+)` with `plus` in the error message. |
| 65 | + |
| 66 | +As you can see from the above, Idris can't verify on its own that `1 + n` is the same thing as `n + 1`. It can accept some help from us, though. If we come up with a *proof* that the above equality holds (or - more generally - that our implementation of addition for natural numbers is *commutative*), we can use this proof to *rewrite* the types on the right hand side of `reverse`. Writing proofs and using `rewrite` will require some in-depth explanations and examples. Therefore, these things will have to wait until another chapter. |
| 67 | + |
| 68 | +## Unrestricted Implicits |
| 69 | + |
| 70 | +In functions like `replicate`, we pass a natural number `n` as an explicit, unrestricted argument from which we infer the length of the vector to return. In some circumstances, `n` can be inferred from the context. For instance, in the following example it is tedious to pass `n` explicitly: |
| 71 | + |
| 72 | +```idris |
| 73 | +ex4 : Vect 3 Integer |
| 74 | +ex4 = zipWith (*) (replicate 3 10) (replicate 3 11) |
| 75 | +``` |
| 76 | + |
| 77 | +The value `n` is clearly derivable from the context, which can be confirmed by replacing it with underscores: |
| 78 | + |
| 79 | +```idris |
| 80 | +ex5 : Vect 3 Integer |
| 81 | +ex5 = zipWith (*) (replicate _ 10) (replicate _ 11) |
| 82 | +``` |
| 83 | + |
| 84 | +We therefore can implement an alternative version of `replicate`, where we pass `n` as an implicit argument of *unrestricted* quantity: |
| 85 | + |
| 86 | +```idris |
| 87 | +replicate' : {n : _} -> a -> Vect n a |
| 88 | +replicate' = replicate n |
| 89 | +``` |
| 90 | + |
| 91 | +Note how, in the implementation of `replicate'`, we can refer to `n` and pass it as an explicit argument to `replicate`. |
| 92 | + |
| 93 | +Deciding whether to pass potentially inferable arguments to a function implicitly or explicitly is a question of how often the arguments actually *are* inferable by Idris. Sometimes it might even be useful to have both versions of a function. Remember, however, that even in case of an implicit argument we can still pass the value explicitly: |
| 94 | + |
| 95 | +```idris |
| 96 | +ex6 : Vect ? Bool |
| 97 | +ex6 = replicate' {n = 2} True |
| 98 | +``` |
| 99 | + |
| 100 | +In the type signature above, the question mark (`?`) means, that Idris should try and figure out the value on its own by unification. This forces us to specify `n` explicitly on the right hand side of `ex6`. |
| 101 | + |
| 102 | +### Pattern Matching on Implicits |
| 103 | + |
| 104 | +The implementation of `replicate'` makes use of function `replicate`, where we could pattern match on the explicit argument `n`. However, it is also possible to pattern match on implicit, named arguments of non-zero quantity: |
| 105 | + |
| 106 | +```idris |
| 107 | +replicate'' : {n : _} -> a -> Vect n a |
| 108 | +replicate'' {n = Z} _ = Nil |
| 109 | +replicate'' {n = S _} v = v :: replicate'' v |
| 110 | +``` |
| 111 | + |
| 112 | +<!-- vi: filetype=idris2:syntax=markdown |
| 113 | +--> |
0 commit comments