1 00:00:00,733 --> 00:00:02,733 I'd like to demonstrate a technique for using types 2 00:00:02,733 --> 00:00:05,633 to guide the construction of functional programs. 3 00:00:05,633 --> 00:00:08,433 I have here a Haskell source file with three functions. 4 00:00:08,433 --> 00:00:09,533 The types are given, 5 00:00:09,533 --> 00:00:11,433 but the implementations are stubbed out. 6 00:00:11,433 --> 00:00:13,033 I'll try to fill in the implementations 7 00:00:13,033 --> 00:00:15,033 using what I know about the types, 8 00:00:15,033 --> 00:00:16,433 but I'll otherwise pretend I don't know 9 00:00:16,433 --> 00:00:18,666 what the functions are meant to do. 10 00:00:19,133 --> 00:00:20,233 The first thing I'll do 11 00:00:20,233 --> 00:00:21,933 is make a new name for 'undefined'. 12 00:00:21,933 --> 00:00:23,433 This isn't really necessary, 13 00:00:23,433 --> 00:00:25,933 but it will make things a bit more meaningful. 14 00:00:26,933 --> 00:00:29,333 So a hole is just something that needs to be filled in. 15 00:00:30,366 --> 00:00:32,133 Now let's look at 'compose'. 16 00:00:32,133 --> 00:00:34,433 We can see from the type that it takes three arguments, 17 00:00:34,433 --> 00:00:37,733 so let's give them names: 'f', 'g' and 'x'. 18 00:00:37,733 --> 00:00:39,533 Now let's pull apart the type of 'compose' 19 00:00:39,533 --> 00:00:41,833 so we can write down the type of each argument. 20 00:00:41,833 --> 00:00:43,733 We'll also write down the type of the hole 21 00:00:43,733 --> 00:00:45,633 which is the same as the result type of 'compose', 22 00:00:45,633 --> 00:00:46,700 which is 'c'. 23 00:00:48,466 --> 00:00:50,066 So we need something of type 'c', 24 00:00:50,066 --> 00:00:51,266 and from the arguments, we see that 25 00:00:51,266 --> 00:00:52,366 the only way we'll get that 26 00:00:52,366 --> 00:00:54,866 is by applying 'f' to something of type 'b'. 27 00:00:54,866 --> 00:00:58,166 So let's replace the hole with an application of 'f'. 28 00:00:58,166 --> 00:00:59,766 We don't yet have anything of type 'b', 29 00:00:59,766 --> 00:01:01,466 so we'll just make a new hole for the argument, 30 00:01:01,466 --> 00:01:02,466 and we'll make a note that 31 00:01:02,466 --> 00:01:04,433 the type of the new hole is 'b'. 32 00:01:05,533 --> 00:01:07,700 Similarly, the only way we'll get something of type 'b' 33 00:01:07,700 --> 00:01:09,800 is by an application of 'g', 34 00:01:09,800 --> 00:01:13,200 so let's replace this hole with an application of 'g'. 35 00:01:13,200 --> 00:01:15,200 We now need a new hole for the argument to 'g', 36 00:01:15,200 --> 00:01:17,200 so the type of the hole must be 'a'. 37 00:01:18,133 --> 00:01:20,133 And finally, we already have an 'x' of type 'a', 38 00:01:20,133 --> 00:01:22,433 so we can just use it to fill in the last hole, 39 00:01:22,433 --> 00:01:24,566 and we've arrived at an implementation. 40 00:01:25,200 --> 00:01:26,733 So you see that the technique is to 41 00:01:26,733 --> 00:01:28,633 write down the types of what we have 42 00:01:28,633 --> 00:01:30,433 starting with what we're given as arguments 43 00:01:30,433 --> 00:01:32,633 and also to write down the types of what we need, 44 00:01:32,633 --> 00:01:34,933 starting with the result we need to return. 45 00:01:34,933 --> 00:01:36,533 As in this example, we can then work 46 00:01:36,533 --> 00:01:37,833 backwards from what we need 47 00:01:37,833 --> 00:01:39,833 filling each hole using what we have, 48 00:01:39,833 --> 00:01:41,033 possibly revealing new holes 49 00:01:41,033 --> 00:01:43,533 that we we subsequently need to fill. 50 00:01:43,533 --> 00:01:45,633 As we'll see shortly, we can also work forwards, 51 00:01:45,633 --> 00:01:47,433 constructing new things from what we have, 52 00:01:47,433 --> 00:01:48,933 with the aim of eventually constructing 53 00:01:48,933 --> 00:01:50,833 something that will fill a hole. 54 00:01:51,100 --> 00:01:52,500 But I'm not really happy with 55 00:01:52,500 --> 00:01:54,200 the way we've gone about this. 56 00:01:54,200 --> 00:01:56,500 For one thing, our type assertions are just comments 57 00:01:56,500 --> 00:01:57,500 and they're not checked 58 00:01:57,500 --> 00:02:00,000 so a mistake will lead to wasted effort. 59 00:02:00,000 --> 00:02:01,300 Secondly, it might be awkward 60 00:02:01,300 --> 00:02:03,700 to track the types of multiple holes. 61 00:02:03,700 --> 00:02:06,000 And finally, we have to work out the types ourselves, 62 00:02:06,000 --> 00:02:07,200 when we know that the compiler 63 00:02:07,200 --> 00:02:09,166 ought to be able to do that for us. 64 00:02:09,633 --> 00:02:10,866 So let's start again, 65 00:02:10,866 --> 00:02:12,366 but this time we'll write our assertions 66 00:02:12,366 --> 00:02:14,866 so they can be checked by the compiler. 67 00:02:14,866 --> 00:02:16,466 For the arguments, we'll add a 'where' clause 68 00:02:16,466 --> 00:02:18,466 with a set of dummy bindings. 69 00:02:18,466 --> 00:02:20,666 Visually, this is similar to the comments we wrote before, 70 00:02:20,666 --> 00:02:23,166 but now the types can be checked. 71 00:02:23,166 --> 00:02:24,866 In case it's not clear what's going on here, 72 00:02:24,866 --> 00:02:26,766 we're just taking each argument to the function, 73 00:02:26,766 --> 00:02:28,666 and binding its value to a wildcard pattern 74 00:02:28,666 --> 00:02:31,566 within the scope of the 'where' clause. 75 00:02:31,566 --> 00:02:32,666 The wildcard pattern ensures 76 00:02:32,666 --> 00:02:34,666 that we don't actually create any new names 77 00:02:34,666 --> 00:02:36,666 so we can't change the meaning of the program, 78 00:02:36,666 --> 00:02:39,100 but the type annotations will be checked. 79 00:02:39,566 --> 00:02:41,633 As it is, the compiler won't accept this, 80 00:02:41,633 --> 00:02:42,833 because in plain Haskell, 81 00:02:42,833 --> 00:02:44,633 type variables in the function signature 82 00:02:44,633 --> 00:02:46,933 are not scoped over the function definition. 83 00:02:46,933 --> 00:02:49,033 so the 'a's, 'b's and 'c's in our assertions 84 00:02:49,033 --> 00:02:52,933 are not recognised as the 'a's, 'b's and 'c's in the signature. 85 00:02:52,933 --> 00:02:55,233 We can fix that by turning on a language extension 86 00:02:55,233 --> 00:02:57,933 called 'ScopedTypeVariables'. 87 00:02:57,933 --> 00:02:59,933 We also need to write an explicit 'forall' 88 00:02:59,933 --> 00:03:03,166 to mark the scope to which we want the type variables bound. 89 00:03:03,666 --> 00:03:05,833 That type-checks, and now we can see that 90 00:03:05,833 --> 00:03:08,233 if we make a mistake in one of our annotations, 91 00:03:08,233 --> 00:03:09,733 for example, here, 92 00:03:09,733 --> 00:03:10,833 we get a type error that tells us 93 00:03:10,833 --> 00:03:12,533 not only the location of the error 94 00:03:12,533 --> 00:03:13,833 but what the type should have been, 95 00:03:13,833 --> 00:03:15,933 in this case, 'a' rather than 'b'. 96 00:03:18,233 --> 00:03:20,133 Let's look at the hole. 97 00:03:20,133 --> 00:03:22,533 Rather than work out the type of the hole myself, 98 00:03:22,533 --> 00:03:24,633 I'd like the compiler to tell me. 99 00:03:24,633 --> 00:03:27,633 I can get it to do that by provoking a type error. 100 00:03:27,633 --> 00:03:29,133 To systematically provoke type errors, 101 00:03:29,133 --> 00:03:31,133 we just need a value of a concrete type 102 00:03:31,133 --> 00:03:32,333 that is different from every type 103 00:03:32,333 --> 00:03:34,200 we might use in our programs. 104 00:03:34,533 --> 00:03:35,933 So let's just make a type 105 00:03:35,933 --> 00:03:37,433 and a corresponding data constructor, 106 00:03:37,433 --> 00:03:40,233 both called Hole, with a capital 'H'. 107 00:03:40,233 --> 00:03:42,033 Now we have two varieties of hole. 108 00:03:42,033 --> 00:03:44,033 I'll call the upper-case variety a noisy Hole, 109 00:03:44,033 --> 00:03:45,833 since it will always provoke a type error, 110 00:03:45,833 --> 00:03:48,033 and I'll call the lower-case variety a silent hole, 111 00:03:48,033 --> 00:03:50,633 since it will always be accepted anywhere. 112 00:03:50,633 --> 00:03:52,333 The idea is that if we have several holes, 113 00:03:52,333 --> 00:03:54,133 we'll use only one noisy Hole at a time, 114 00:03:54,133 --> 00:03:56,433 and leave the rest as silent holes. 115 00:03:56,433 --> 00:03:58,033 That way, when we're looking at an error message 116 00:03:58,033 --> 00:03:59,533 provoked by a noisy Hole, 117 00:03:59,533 --> 00:04:00,533 we don't have to think about 118 00:04:00,533 --> 00:04:02,866 which Hole caused that error. 119 00:04:03,233 --> 00:04:06,200 Let's make this hole noisy. 120 00:04:06,200 --> 00:04:08,200 If we look below, the error message tells us that 121 00:04:08,200 --> 00:04:11,600 GHC was expecting a 'c' instead of a Hole. 122 00:04:11,600 --> 00:04:13,200 Using the same reasoning as before, 123 00:04:13,200 --> 00:04:15,400 we replace the Hole with an application of 'f', 124 00:04:15,400 --> 00:04:16,700 and now the compiler tells us that 125 00:04:16,700 --> 00:04:19,100 the new Hole needs to be filled with a 'b'. 126 00:04:19,100 --> 00:04:21,000 So we replace that with an application of 'g', 127 00:04:21,000 --> 00:04:23,600 and now the new Hole needs to filled with an 'a'. 128 00:04:23,600 --> 00:04:26,433 And finally, we can satisfy that with an 'x'. 129 00:04:26,966 --> 00:04:28,666 Now, because the noisy Hole is a type 130 00:04:28,666 --> 00:04:29,766 as well as a value, 131 00:04:29,766 --> 00:04:31,666 we can also use it in type contexts. 132 00:04:31,666 --> 00:04:33,866 For example, if we weren't sure of the type of 'x' 133 00:04:33,866 --> 00:04:35,666 while writing assertions about the arguments, 134 00:04:35,666 --> 00:04:38,766 we can just use a noisy Hole to ask the compiler. 135 00:04:38,766 --> 00:04:40,166 So this error message tells us that 136 00:04:40,166 --> 00:04:42,166 the Hole should have been an 'a'. 137 00:04:42,533 --> 00:04:43,733 Now that we're done, 138 00:04:43,733 --> 00:04:46,233 we can remove the superfluous dummy bindings, 139 00:04:46,233 --> 00:04:48,333 and since we're no longer referring to type variables 140 00:04:48,333 --> 00:04:49,733 in the body of the function, 141 00:04:49,733 --> 00:04:52,033 we can also remove the 'forall' binders. 142 00:04:52,366 --> 00:04:54,333 So much for 'compose'. 143 00:04:54,333 --> 00:04:57,033 Let's move on to a slightly more interesting example. 144 00:04:57,033 --> 00:04:58,233 In the type of 'apply', 145 00:04:58,233 --> 00:05:01,133 we see that the variable 'm' stands for a type constructor, 146 00:05:01,133 --> 00:05:02,733 and we can further see that it is constrained 147 00:05:02,733 --> 00:05:05,833 to the type-constructor class 'Monad'. 148 00:05:05,833 --> 00:05:07,633 The constraint means that we know more about 'm' 149 00:05:07,633 --> 00:05:09,133 than if it were unconstrained. 150 00:05:09,133 --> 00:05:10,633 In particular, we know that we can, 151 00:05:10,633 --> 00:05:12,033 and indeed will probably have to make use of 152 00:05:12,033 --> 00:05:14,233 the methods of the 'Monad' type-constructor class 153 00:05:14,233 --> 00:05:16,066 in our implementation. 154 00:05:16,500 --> 00:05:19,000 Proceeding as before, we see from the type that 155 00:05:19,000 --> 00:05:20,700 'apply' takes two arguments, 156 00:05:20,700 --> 00:05:23,200 so we'll name them 'mf' and 'ma'. 157 00:05:23,200 --> 00:05:25,866 We'll write assertions for the types of the arguments. 158 00:05:28,433 --> 00:05:29,866 And, of course, we need to remember 159 00:05:29,866 --> 00:05:33,566 to explicitly bind the type variables in the signature. 160 00:05:33,566 --> 00:05:35,566 OK, so that compiles now. 161 00:05:35,566 --> 00:05:36,866 But remember that if we weren't sure of 162 00:05:36,866 --> 00:05:37,866 the type of an argument 163 00:05:37,866 --> 00:05:40,466 we can use a noisy Hole to ask the compiler. 164 00:05:40,466 --> 00:05:41,966 Here it's telling us that it was expecting 165 00:05:41,966 --> 00:05:44,666 'mf' to have the type 'm' of 'a' to 'b'. 166 00:05:45,633 --> 00:05:47,566 Looking back at the implementation, 167 00:05:47,566 --> 00:05:49,266 if we make our Hole noisy, we see that we need to 168 00:05:49,266 --> 00:05:51,766 construct something of type 'm b'. 169 00:05:51,766 --> 00:05:52,866 Clearly, we can't do that 170 00:05:52,866 --> 00:05:54,766 with a simple application of what we have, 171 00:05:54,766 --> 00:05:56,166 so we're going to have make use of the fact that 172 00:05:56,166 --> 00:05:57,466 'm' is a Monad. 173 00:05:57,866 --> 00:05:59,466 Now, if we need to remind ourselves 174 00:05:59,466 --> 00:06:02,266 of the type of any function or method we want to use, 175 00:06:02,266 --> 00:06:04,966 we could use a GHCi query, or alternatively, 176 00:06:04,966 --> 00:06:06,666 we can use a dummy binding. 177 00:06:06,666 --> 00:06:08,166 In particular, we can use a dummy binding 178 00:06:08,166 --> 00:06:09,166 to check whether we can 179 00:06:09,166 --> 00:06:11,566 specialise any variables in the type of the function 180 00:06:11,566 --> 00:06:14,333 to the particular types that we want to use. 181 00:06:14,800 --> 00:06:16,733 For example, if we add a dummy binding 182 00:06:16,733 --> 00:06:18,733 for the monadic 'bind' operator 183 00:06:18,733 --> 00:06:21,233 we can use a noisy Hole to ask for its type. 184 00:06:21,233 --> 00:06:22,933 For reasons I don't quite understand, 185 00:06:22,933 --> 00:06:24,633 GHC doesn't tell us the full story, 186 00:06:24,633 --> 00:06:26,933 but it's enough to get us by. 187 00:06:26,933 --> 00:06:29,333 Notice that the error uses fresh type variables, 188 00:06:29,333 --> 00:06:31,933 'm0', 'a0' and 'b0'. 189 00:06:31,933 --> 00:06:33,633 These are universally quantified, which means 190 00:06:33,633 --> 00:06:36,833 we should be able to instantiate them to anything we like. 191 00:06:36,833 --> 00:06:38,833 Since we want to construct an 'm b', 192 00:06:38,833 --> 00:06:39,933 it seems likely that we'll want 193 00:06:39,933 --> 00:06:42,633 the 'bind' operator to return 'm b' as well, 194 00:06:42,633 --> 00:06:43,833 so we might as well specialise 195 00:06:43,833 --> 00:06:48,533 by instantiating 'm0' and 'b0' with 'm' and 'b' respectively. 196 00:06:48,533 --> 00:06:50,733 But since I'm not sure what 'a0' will be, 197 00:06:50,733 --> 00:06:52,333 I'll leave that polymorphic for now, 198 00:06:52,333 --> 00:06:55,533 and, in fact, I'll write an explicit 'forall' to make this clear, 199 00:06:55,533 --> 00:06:57,133 and I'll rename 'a0' to 'h' 200 00:06:57,133 --> 00:07:01,433 to avoid any confusion with the type variable 'a'. 201 00:07:01,433 --> 00:07:03,533 This now passes the type checker, which means that 202 00:07:03,533 --> 00:07:06,666 this is a valid partial specialisation. 203 00:07:07,100 --> 00:07:08,433 Now, we have two choices 204 00:07:08,433 --> 00:07:12,133 for applying the bind operator: 'mf' and 'ma'. 205 00:07:12,133 --> 00:07:14,033 If we want to, we can use dummy bindings 206 00:07:14,033 --> 00:07:16,033 to explore the resulting types. 207 00:07:16,033 --> 00:07:18,733 For example, if we partially apply "bind' to 'mf', 208 00:07:18,733 --> 00:07:19,833 this will swallow the first parameter. 209 00:07:19,833 --> 00:07:20,733 this will swallow the first parameter. 210 00:07:20,733 --> 00:07:23,433 Since this will also instantiate the type variable 'h', 211 00:07:23,433 --> 00:07:26,066 we can use a noisy Hole to find out its type. 212 00:07:28,800 --> 00:07:30,266 And, of course, we can do the same 213 00:07:30,266 --> 00:07:33,433 for a partial application of 'bind' to 'ma'. 214 00:07:34,666 --> 00:07:37,033 OK, back to the implementation. 215 00:07:37,033 --> 00:07:39,633 Without anything else to tell us which argument to bind first, 216 00:07:39,633 --> 00:07:40,833 we'll just follow convention, 217 00:07:40,833 --> 00:07:44,133 and bind the left-most argument first. 218 00:07:44,133 --> 00:07:47,533 So we replace our Hole with 'mf' bound to a new Hole. 219 00:07:47,533 --> 00:07:50,233 We see that the new Hole requires a function of one argument, 220 00:07:50,233 --> 00:07:51,433 and in order to make assertions 221 00:07:51,433 --> 00:07:52,733 about the type of the argument, 222 00:07:52,733 --> 00:07:55,933 we need a name and a scope to write those assertions, 223 00:07:55,933 --> 00:07:58,633 which means we also need to name the function. 224 00:07:58,633 --> 00:08:00,733 So we'll name the function 'k', 225 00:08:00,733 --> 00:08:01,933 and its argument 'f', 226 00:08:01,933 --> 00:08:03,900 and we'll use a silent hole for the result of 'k' 227 00:08:03,900 --> 00:08:07,200 while we're dealing with assertions about the type of 'f'. 228 00:08:07,200 --> 00:08:10,733 Writing the assertion, we find that 'f' has type 'a' to 'b'. 229 00:08:12,966 --> 00:08:15,833 Now, switching to a noisy Hole for the result of 'k', 230 00:08:15,833 --> 00:08:18,233 we see that again we need to construct an 'm b'. 231 00:08:18,233 --> 00:08:19,633 We still have no way to do this with 232 00:08:19,633 --> 00:08:21,733 a simple application of of what we have, 233 00:08:21,733 --> 00:08:23,533 so we turn to the monadic 'bind' operator, 234 00:08:23,533 --> 00:08:25,200 this time on 'ma'. 235 00:08:25,933 --> 00:08:27,466 Again, the new Hole requires 236 00:08:27,466 --> 00:08:28,866 a function of a single argument, 237 00:08:28,866 --> 00:08:31,166 so we'll name the function 'r', 238 00:08:31,166 --> 00:08:32,666 and the argument 'x', 239 00:08:32,666 --> 00:08:35,466 and we'll write an assertion for the type of 'x', 240 00:08:35,466 --> 00:08:37,800 using a noisy Hole to ask for the type. 241 00:08:37,800 --> 00:08:40,600 This time the form of the error message is different, 242 00:08:40,600 --> 00:08:42,500 but the interpretation is the same: 243 00:08:42,500 --> 00:08:45,033 we need an 'a' in place of the Hole. 244 00:08:45,733 --> 00:08:47,800 Returning to the result of the function 'r', 245 00:08:47,800 --> 00:08:51,300 we see that GHC is expecting something of type 'm b0', 246 00:08:51,300 --> 00:08:53,100 where 'b0' is a fresh type variable, 247 00:08:53,100 --> 00:08:56,300 which implies that it is universally quantified. 248 00:08:56,300 --> 00:08:58,000 In this case, it appears that GHC has 249 00:08:58,000 --> 00:09:01,000 generalised the type it is expecting of 'r'. 250 00:09:01,000 --> 00:09:02,900 Although it's not clear to me exactly when 251 00:09:02,900 --> 00:09:05,400 GHC will perform this generalisation, 252 00:09:05,400 --> 00:09:07,400 to see that it's reasonable for it to do so, 253 00:09:07,400 --> 00:09:09,400 consider that if 'r' is polymorphic enough 254 00:09:09,400 --> 00:09:11,500 to allow any type 'b0', 255 00:09:11,500 --> 00:09:14,566 then clearly it can allow the specific type 'b'. 256 00:09:15,133 --> 00:09:16,866 The problem is that we don't want 257 00:09:16,866 --> 00:09:19,166 to implement such a polymorphic 'r'. 258 00:09:19,166 --> 00:09:22,366 In fact, in this case, that would be impossible. 259 00:09:22,366 --> 00:09:23,466 Instead, we want to implement 260 00:09:23,466 --> 00:09:24,966 the most specific type we can, 261 00:09:24,966 --> 00:09:26,466 because that is likely to be easier than 262 00:09:26,466 --> 00:09:29,266 implementing a more general type. 263 00:09:29,266 --> 00:09:31,766 So, if we're not sure what the specific type should be, 264 00:09:31,766 --> 00:09:34,166 how can we find out from the compiler? 265 00:09:34,166 --> 00:09:35,566 The trick is to move the noisy Hole 266 00:09:35,566 --> 00:09:38,366 to the relevant place in a type annotation. 267 00:09:38,366 --> 00:09:39,866 Then GHC is happy to tell us that 268 00:09:39,866 --> 00:09:42,433 we merely need a 'b' in place of the Hole. 269 00:09:43,066 --> 00:09:45,066 Now, we still have no way to directly construct 270 00:09:45,066 --> 00:09:46,766 something of type 'm b'. 271 00:09:46,766 --> 00:09:48,566 But we do have an 'f' of type 'a' to 'b', 272 00:09:48,566 --> 00:09:50,466 and an 'x' of type 'a', 273 00:09:50,466 --> 00:09:52,266 so we can construct 'f' of 'x', 274 00:09:52,266 --> 00:09:55,366 and use an assertion to check its type. 275 00:09:55,366 --> 00:09:57,266 Finally, to get from a 'b' to a 'm b', 276 00:09:57,266 --> 00:09:58,966 we once again need to make use of the fact 277 00:09:58,966 --> 00:10:00,966 that 'm' is a Monad. 278 00:10:00,966 --> 00:10:02,566 If we want, we can use a dummy binding 279 00:10:02,566 --> 00:10:03,566 to check that we can make 280 00:10:03,566 --> 00:10:06,366 a suitable specialisation of the type of 'return'. 281 00:10:06,366 --> 00:10:09,766 Then we can check that 'return' of 'f' of 'x' has the right type, 282 00:10:09,766 --> 00:10:12,400 and since it does, we can fill our last hole. 283 00:10:12,933 --> 00:10:14,400 Things have become a little messy, 284 00:10:14,400 --> 00:10:16,300 so let's back-substitute. 285 00:10:16,300 --> 00:10:20,800 Here, 'k' becomes 'lambda f' to 'ma' bound to 'r', 286 00:10:20,800 --> 00:10:23,000 but since 'r' is not in scope here, 287 00:10:23,000 --> 00:10:26,900 we immediately substitute 'lambda x' to 'return' of 'f' of 'x'. 288 00:10:26,900 --> 00:10:29,300 We no longer need the dummy bindings, 289 00:10:29,300 --> 00:10:30,900 nor do we need the explicit binders 290 00:10:30,900 --> 00:10:32,633 for the type variables in the signature. 291 00:10:33,266 --> 00:10:35,933 At this point, we could convert this to 'do'-notation, 292 00:10:35,933 --> 00:10:38,733 or simplify using 'liftM', or both, 293 00:10:38,733 --> 00:10:41,000 but I'll leave that for another time. 294 00:10:41,600 --> 00:10:43,333 Instead, if you're not already exhausted, 295 00:10:43,333 --> 00:10:45,533 let's do one final example. 296 00:10:45,533 --> 00:10:46,833 Here, we'll see that when we encounter 297 00:10:46,833 --> 00:10:48,533 concrete types and type constructors, 298 00:10:48,533 --> 00:10:49,633 we typically have to make 299 00:10:49,633 --> 00:10:51,733 more choices about our implementation. 300 00:10:52,266 --> 00:10:53,866 We can see from the type that 301 00:10:53,866 --> 00:10:55,766 'filterM' takes two arguments. 302 00:10:55,766 --> 00:10:57,366 Let's name them 'p' and 'xs', 303 00:10:57,366 --> 00:11:01,266 and as usual, let's write assertions about their types. 304 00:11:04,266 --> 00:11:05,366 And, let's not forget to write 305 00:11:05,366 --> 00:11:07,366 explicit binders for the type variables. 306 00:11:07,866 --> 00:11:09,233 Now, I'm pretty sure I already know 307 00:11:09,233 --> 00:11:10,333 the type of the hole, 308 00:11:10,333 --> 00:11:12,333 so I'll just write that in there. 309 00:11:12,333 --> 00:11:14,533 Again, we can't construct an 'm' of list of 'a' 310 00:11:14,533 --> 00:11:16,333 by a simple application of what we have, 311 00:11:16,333 --> 00:11:18,933 nor do we have any monadic value to bind. 312 00:11:18,933 --> 00:11:20,333 But we do have a list of 'a', 313 00:11:20,333 --> 00:11:22,033 so we could either pattern-match on 'xs' 314 00:11:22,033 --> 00:11:24,833 or apply some list function to it. 315 00:11:24,833 --> 00:11:27,333 But which list function would we apply? 316 00:11:27,333 --> 00:11:28,433 There are many list functions, 317 00:11:28,433 --> 00:11:30,433 so it's not an easy question to answer, 318 00:11:30,433 --> 00:11:32,433 but since list is a recursive structure, 319 00:11:32,433 --> 00:11:34,633 the most useful solution is likely to involve 320 00:11:34,633 --> 00:11:36,733 recursion over 'xs'. 321 00:11:36,733 --> 00:11:38,733 And the right-fold function, 'foldr', 322 00:11:38,733 --> 00:11:42,000 captures the most general recursion scheme over lists. 323 00:11:42,466 --> 00:11:43,633 So let's replace the hole with 324 00:11:43,633 --> 00:11:46,033 an application of 'foldr' to 'xs', 325 00:11:46,033 --> 00:11:47,133 leaving two new holes 326 00:11:47,133 --> 00:11:49,333 for the remaining arguments. 327 00:11:49,333 --> 00:11:50,533 The second of these arguments 328 00:11:50,533 --> 00:11:52,933 corresponds to the base case for the recursion. 329 00:11:52,933 --> 00:11:56,433 In other words, it's the result when 'xs' is empty. 330 00:11:56,433 --> 00:11:57,833 And indeed, using a noisy Hole, 331 00:11:57,833 --> 00:11:59,033 we see that it must have type 332 00:11:59,033 --> 00:12:01,333 'm' of list of 'a'. 333 00:12:01,333 --> 00:12:02,533 As in the previous example, 334 00:12:02,533 --> 00:12:04,433 we can use 'return' to construct one of those 335 00:12:04,433 --> 00:12:06,033 from a list of 'a', 336 00:12:06,033 --> 00:12:08,233 and the only list of 'a' we can construct out of thin air 337 00:12:08,233 --> 00:12:09,733 is the empty list, 338 00:12:09,733 --> 00:12:11,233 so we should be able to replace this Hole 339 00:12:11,233 --> 00:12:13,100 with 'return' of the empty list, 340 00:12:14,666 --> 00:12:15,900 Now, looking at the other Hole, 341 00:12:15,900 --> 00:12:17,200 we see that GHC has again 342 00:12:17,200 --> 00:12:19,800 generalised the type a little more than we'd like, 343 00:12:19,800 --> 00:12:20,900 but we can at least see that we need 344 00:12:20,900 --> 00:12:22,800 a function of two arguments, 345 00:12:22,800 --> 00:12:24,900 so let's name the function 'f', 346 00:12:24,900 --> 00:12:27,900 and its arguments 'x' and 'r', 347 00:12:27,900 --> 00:12:29,400 and let's write an assertion to find out 348 00:12:29,400 --> 00:12:33,500 the type of 'x', which is 'a'. 349 00:12:33,500 --> 00:12:36,200 Similarly, we find that the type of 'r' 350 00:12:36,200 --> 00:12:37,933 is 'm' of list of 'a'. 351 00:12:39,033 --> 00:12:41,733 Next, we look at the type of the result of 'f', 352 00:12:41,733 --> 00:12:44,533 which we see should also be 'm' of list of 'a'. 353 00:12:44,533 --> 00:12:46,133 Obviously, we could satisfy the types 354 00:12:46,133 --> 00:12:47,533 by simply returning 'r', 355 00:12:47,533 --> 00:12:48,733 but that gives a trivial solution 356 00:12:48,733 --> 00:12:51,133 which is not useful. 357 00:12:51,133 --> 00:12:52,433 Instead, we notice that we haven't yet 358 00:12:52,433 --> 00:12:54,133 used the argument 'p', 359 00:12:54,133 --> 00:12:56,933 which is a function from 'a' to 'm' of Bool. 360 00:12:56,933 --> 00:12:58,533 Since we have an 'x' of type 'a', 361 00:12:58,533 --> 00:13:01,233 we can apply 'p' to 'x' to get an 'm' of Bool, 362 00:13:01,233 --> 00:13:02,433 and since 'm' is a Monad, 363 00:13:02,433 --> 00:13:04,400 we can bind the result to a new Hole. 364 00:13:04,933 --> 00:13:06,266 Now we see that the new Hole 365 00:13:06,266 --> 00:13:07,766 requires a function of one argument, 366 00:13:07,766 --> 00:13:09,566 so we name it 'k', 367 00:13:09,566 --> 00:13:11,166 and its argument 'c', 368 00:13:11,166 --> 00:13:12,366 and we use an assertion to find that 369 00:13:12,366 --> 00:13:14,433 the type of 'c' is Bool. 370 00:13:15,433 --> 00:13:17,666 Looking back at the type of the result of 'k', 371 00:13:17,666 --> 00:13:20,266 we see that GHC generalises the type, 372 00:13:20,266 --> 00:13:21,466 so we use the usual trick 373 00:13:21,466 --> 00:13:23,766 to get a more specific type for 'b0', 374 00:13:23,766 --> 00:13:26,000 and that turns out to be list of 'a'. 375 00:13:26,533 --> 00:13:28,100 Now, to get a non-trivial result, 376 00:13:28,100 --> 00:13:30,200 we should really do something with 'c'. 377 00:13:30,200 --> 00:13:33,500 Since 'c' is a Bool, the natural thing to do is branch, 378 00:13:33,500 --> 00:13:36,800 so let's replace the hole with a branch on 'c'. 379 00:13:36,800 --> 00:13:39,800 This gives us two new holes, one for each branch. 380 00:13:39,800 --> 00:13:41,200 Now we just need to come up with two 381 00:13:41,200 --> 00:13:42,800 meaningfully different ways to construct 382 00:13:42,800 --> 00:13:45,500 an 'm' of list of 'a' from 'x' and 'r'. 383 00:13:46,066 --> 00:13:47,633 There are many ways to do this, 384 00:13:47,633 --> 00:13:49,133 but the one seems most meaningful 385 00:13:49,133 --> 00:13:51,033 is the one which relates each condition 'c' 386 00:13:51,033 --> 00:13:53,833 most directly to the 'x' which produced it. 387 00:13:53,833 --> 00:13:55,833 So therefore, we'll use 'x' if and only if 388 00:13:55,833 --> 00:13:58,333 the condition 'c' is True. 389 00:13:58,333 --> 00:14:01,333 In the False case, we'll just return 'r'. 390 00:14:01,833 --> 00:14:03,100 Now, in the True case, 391 00:14:03,100 --> 00:14:05,300 we want to combine 'x' and 'r'. 392 00:14:05,300 --> 00:14:06,700 If we had a little experience with monads, 393 00:14:06,700 --> 00:14:09,000 we might recognise that 'liftM' would do the job, 394 00:14:09,000 --> 00:14:12,500 like this, but suppose we don't see that. 395 00:14:12,500 --> 00:14:14,400 Then, our only real option is to bind 'r', 396 00:14:14,400 --> 00:14:15,700 which is a monadic value, 397 00:14:15,700 --> 00:14:18,000 to a new Hole. 398 00:14:18,000 --> 00:14:19,600 The new Hole requires a function, 399 00:14:19,600 --> 00:14:21,500 so we name it 'j', 400 00:14:21,500 --> 00:14:23,733 and name its argument 'ys', 401 00:14:25,533 --> 00:14:26,600 which GHC tells us 402 00:14:26,600 --> 00:14:28,166 should have type list of 'a'. 403 00:14:28,733 --> 00:14:29,733 When we try to discover 404 00:14:29,733 --> 00:14:31,133 the type of the result of 'j', 405 00:14:31,133 --> 00:14:32,933 we run into a new problem. 406 00:14:32,933 --> 00:14:33,933 Previously, we have only seen 407 00:14:33,933 --> 00:14:35,633 over-generalised type variables, 408 00:14:35,633 --> 00:14:37,033 but this time GHC has given us 409 00:14:37,033 --> 00:14:40,733 an over-generalised type constructor variable 'm0'. 410 00:14:40,733 --> 00:14:43,933 Our usual trick to discover a more specific type won't work, 411 00:14:43,933 --> 00:14:46,333 because Hole has the wrong kind. 412 00:14:46,333 --> 00:14:47,433 We just get a kind error, 413 00:14:47,433 --> 00:14:49,933 which doesn't tell us anything about the types. 414 00:14:49,933 --> 00:14:51,733 But we can introduce a hole constructor 415 00:14:51,733 --> 00:14:53,133 with the right kind. 416 00:14:53,133 --> 00:14:54,233 Let's call it 'Hole1', 417 00:14:54,233 --> 00:14:57,033 and notice that it takes a type argument. 418 00:14:57,033 --> 00:14:59,133 Then, when we try to set the result type of 'j' 419 00:14:59,133 --> 00:15:01,333 to 'Hole1 Hole', 420 00:15:01,333 --> 00:15:02,733 GHC tells us first that it expected 421 00:15:02,733 --> 00:15:04,400 'm' instead of 'Hole1' 422 00:15:05,666 --> 00:15:07,733 And then list of 'a' instead of 'Hole'. 423 00:15:09,400 --> 00:15:11,700 Now that we have 'x' and 'ys', 424 00:15:11,700 --> 00:15:14,033 we can combine them to make a new list, 425 00:15:14,500 --> 00:15:16,066 and use the monadic 'return' 426 00:15:16,066 --> 00:15:19,466 to construct a value of the right type. 427 00:15:19,466 --> 00:15:21,066 Since that fills our last hole, 428 00:15:21,066 --> 00:15:22,266 and since we've used all of the arguments 429 00:15:22,266 --> 00:15:24,966 to filterM' in a meaningful way, 430 00:15:24,966 --> 00:15:26,266 we've arrived at a non-trivial, 431 00:15:26,266 --> 00:15:28,300 and hopefully useful implementation. 432 00:15:28,566 --> 00:15:30,166 In fact, this implementation is 433 00:15:30,166 --> 00:15:32,666 equivalent to 'filterM' in the standard library. 434 00:15:33,066 --> 00:15:36,100 Let's just clean up by back-substituting 'k', 435 00:15:38,666 --> 00:15:40,966 and then 'j', 436 00:15:42,766 --> 00:15:45,433 and then removing superfluous dummy bindings, 437 00:15:45,433 --> 00:15:49,733 'forall' binders and type annotations. 438 00:15:49,733 --> 00:15:50,933 Finally, we can disable 439 00:15:50,933 --> 00:15:52,633 the 'ScopedTypeVariables' extension, 440 00:15:52,633 --> 00:15:53,933 and remove the hole definitions 441 00:15:53,933 --> 00:15:55,133 to make absolutely sure there's 442 00:15:55,133 --> 00:15:57,833 nothing left to fill in. 443 00:15:57,833 --> 00:15:59,066 And we're done. 444 00:15:59,533 --> 00:16:00,900 To summarise, we've seen an approach for 445 00:16:00,900 --> 00:16:02,400 using types to guide the construction 446 00:16:02,400 --> 00:16:03,600 of functional programs, 447 00:16:03,600 --> 00:16:04,700 which consists of writing down 448 00:16:04,700 --> 00:16:05,900 the types of what we have, 449 00:16:05,900 --> 00:16:07,700 and the types of what we need, 450 00:16:07,700 --> 00:16:10,400 and systematically joining the dots in between. 451 00:16:10,400 --> 00:16:11,500 We've also seen some tricks 452 00:16:11,500 --> 00:16:13,366 for getting some help from GHC. 453 00:16:13,900 --> 00:16:14,900 But don't confuse the tricks 454 00:16:14,900 --> 00:16:16,600 with the underlying approach. 455 00:16:16,600 --> 00:16:18,100 The underlying approach is timeless, 456 00:16:18,100 --> 00:16:20,000 and in fact comes from mathematical logic, 457 00:16:20,000 --> 00:16:22,300 where it's called natural deduction. 458 00:16:22,300 --> 00:16:23,600 The tricks are only really applicable 459 00:16:23,600 --> 00:16:25,000 to current versions of GHC, 460 00:16:25,000 --> 00:16:27,700 as of early 2013. 461 00:16:27,700 --> 00:16:29,100 In fact, sometime in the next few months, 462 00:16:29,100 --> 00:16:30,600 we expect a release of GHC 463 00:16:30,600 --> 00:16:32,200 which is likely to include a new extension 464 00:16:32,200 --> 00:16:34,000 called 'TypeHoles', 465 00:16:34,000 --> 00:16:35,300 which will make development 466 00:16:35,300 --> 00:16:37,900 in the natural deduction style considerable smoother.