[Script Info]
Title: 
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:00.00,0:00:19.37,Default,,0000,0000,0000,,{\i1}36C3 preroll music{\i0}
Dialogue: 0,0:00:19.37,0:00:25.55,Default,,0000,0000,0000,,Herald: Our next talk is held by Mike\NSperber, and he is already very ready for
Dialogue: 0,0:00:25.55,0:00:31.01,Default,,0000,0000,0000,,that. He's head of a software company in\NTübingen in Germany and he's going to talk
Dialogue: 0,0:00:31.01,0:00:36.54,Default,,0000,0000,0000,,about "Getting software right with\Nproperties, generator tests and proofs".
Dialogue: 0,0:00:36.54,0:00:42.47,Default,,0000,0000,0000,,And the main thing here is functional\Nprogramming. One tiny thing you might not
Dialogue: 0,0:00:42.47,0:00:50.74,Default,,0000,0000,0000,,know about him is that 1986 he won a\Nfederal competition on IT and so give him
Dialogue: 0,0:00:50.74,0:00:53.87,Default,,0000,0000,0000,,a warm applause for that and also for his\Ntalk.
Dialogue: 0,0:00:53.87,0:00:58.22,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:00:58.22,0:01:04.69,Default,,0000,0000,0000,,Mike Sperber: Thank you very much. So is\Nanybody actively using the induction loop
Dialogue: 0,0:01:04.69,0:01:09.11,Default,,0000,0000,0000,,feature in the first couple of rows? Cuz\NI know somebody who would like to know.
Dialogue: 0,0:01:09.11,0:01:17.08,Default,,0000,0000,0000,,Not right now. Okay. Anyway, so let me get\None shameless plug of advertising out of
Dialogue: 0,0:01:17.08,0:01:22.23,Default,,0000,0000,0000,,the way. If you find the contents of this\Ntalk interesting, we're running a
Dialogue: 0,0:01:22.23,0:01:26.17,Default,,0000,0000,0000,,developer conference in Berlin in February\Ncalled Bob, which is very friendly and
Dialogue: 0,0:01:26.17,0:01:32.58,Default,,0000,0000,0000,,very nice, very tiny compared to this one.\NAnd we'd love to see you there. Another
Dialogue: 0,0:01:32.58,0:01:39.57,Default,,0000,0000,0000,,thing, this is an introductory talk. So if\Nyou were expecting the latest developments
Dialogue: 0,0:01:39.57,0:01:44.28,Default,,0000,0000,0000,,on proof tactic, in fact, if you know what\Nproof tactic is, then all you might get
Dialogue: 0,0:01:44.28,0:01:48.89,Default,,0000,0000,0000,,from this talk is sort of mild amusement.\NAnd I won't be mad at you at all if you go
Dialogue: 0,0:01:48.89,0:01:56.16,Default,,0000,0000,0000,,for one of the more exciting talks. Ok?\NSo. Or leave at any time. That's perfectly
Dialogue: 0,0:01:56.16,0:02:01.79,Default,,0000,0000,0000,,fine, if this material is not for you.\NSpeaking of introductory talks, here's a
Dialogue: 0,0:02:01.79,0:02:05.74,Default,,0000,0000,0000,,piece of code written in the language that\NI will use for this talk and it's called
Dialogue: 0,0:02:05.74,0:02:12.16,Default,,0000,0000,0000,,Idris. Who has written an Idris program\Nbefore? Very good. Ok. Oh, there's one
Dialogue: 0,0:02:12.16,0:02:17.81,Default,,0000,0000,0000,,person back there. That means if any part\Nof this program, as soon as I'm done
Dialogue: 0,0:02:17.81,0:02:22.13,Default,,0000,0000,0000,,explaining, is not clear to you, it's also\Nnot clear to two or three hundred other
Dialogue: 0,0:02:22.13,0:02:26.54,Default,,0000,0000,0000,,people in this room. And I would love to\Nhave your help. Interrupt me, ask a
Dialogue: 0,0:02:26.54,0:02:30.25,Default,,0000,0000,0000,,question anytime in the talk if there's\Nanything here not clear. It's going to
Dialogue: 0,0:02:30.25,0:02:34.80,Default,,0000,0000,0000,,get, even though it's meant to be\Nintroductory, will get quite technical at
Dialogue: 0,0:02:34.80,0:02:41.12,Default,,0000,0000,0000,,times. So let me try explaining this one.\NSo this is a classic example in functional
Dialogue: 0,0:02:41.12,0:02:46.14,Default,,0000,0000,0000,,programming that I use often in my talks,\Nabout animals on the Texas Highway. And if
Dialogue: 0,0:02:46.14,0:02:49.68,Default,,0000,0000,0000,,you can see there, the central definition\Nsays data Animal. That's the data
Dialogue: 0,0:02:49.68,0:02:54.19,Default,,0000,0000,0000,,definition of animals. And in this\Nparticular version of the Texas Highway,
Dialogue: 0,0:02:54.19,0:02:58.19,Default,,0000,0000,0000,,there's two different kinds of animals.\NThere is Armadillo, it's where it says
Dialogue: 0,0:02:58.19,0:03:03.86,Default,,0000,0000,0000,,Dillo there. And there's Parrots, for some\Nreason, on the Texas Highway. Does that
Dialogue: 0,0:03:03.86,0:03:07.39,Default,,0000,0000,0000,,make sense? Two different kinds of\Nanimals. And you see that definition.
Dialogue: 0,0:03:07.39,0:03:14.43,Default,,0000,0000,0000,,Yeah, nod, that greatly helps me. And if\Nyou see those two definitions for Dillo
Dialogue: 0,0:03:14.43,0:03:18.53,Default,,0000,0000,0000,,and Parrot, you can see, while the arrows\Nare kind of funny, but you can see that
Dialogue: 0,0:03:18.53,0:03:23.93,Default,,0000,0000,0000,,Dillo and Parrots have two properties\Neach, and it says their Liveness. That's
Dialogue: 0,0:03:23.93,0:03:27.69,Default,,0000,0000,0000,,one of the properties of an armadillo. And\Nup there at the very top, you see the
Dialogue: 0,0:03:27.69,0:03:31.52,Default,,0000,0000,0000,,definition of Liveness, it says Liveness\Nmeans dead or alive. It's an armadillo,
Dialogue: 0,0:03:31.52,0:03:36.92,Default,,0000,0000,0000,,can be dead or alive on the Texas Highway.\NAnd there's also the Weight. And well, you
Dialogue: 0,0:03:36.92,0:03:41.71,Default,,0000,0000,0000,,see, this colon thing is the type\Nsignature for the constructor for
Dialogue: 0,0:03:41.71,0:03:45.98,Default,,0000,0000,0000,,armadillos. So it says there's a liveness\Ngoing on, there's a weight going on, and
Dialogue: 0,0:03:45.98,0:03:49.99,Default,,0000,0000,0000,,then it constructs an animal. And for a\NParrot, there's a string. Every parrot
Dialogue: 0,0:03:49.99,0:03:54.15,Default,,0000,0000,0000,,speaks, right? And so it's the sentence\Nthe Parrot says, and also the Weight. And
Dialogue: 0,0:03:54.15,0:03:58.59,Default,,0000,0000,0000,,it also produces an animal. And, up there,\Nyou can see the definition of Weight is
Dialogue: 0,0:03:58.59,0:04:02.44,Default,,0000,0000,0000,,for simplicity's sake, I'm saying that\NWeight is a type. So that's kind of
Dialogue: 0,0:04:02.44,0:04:06.15,Default,,0000,0000,0000,,unusual for Idris, but you don't have to\Nworry about it. But you can see there,
Dialogue: 0,0:04:06.15,0:04:10.83,Default,,0000,0000,0000,,Weight is just the same thing as an\Ninteger. And if you look down there, where
Dialogue: 0,0:04:10.83,0:04:16.55,Default,,0000,0000,0000,,it says a1, a2 and a3, that has three\Nexamples for animals. So it says a1:
Dialogue: 0,0:04:16.55,0:04:21.48,Default,,0000,0000,0000,,Animal, just to say that a1 is an animal.\NSo, Idris is a language that always has
Dialogue: 0,0:04:21.48,0:04:26.61,Default,,0000,0000,0000,,type declarations. And it says a1 is Dillo\NAlive 10. And that means it's an
Dialogue: 0,0:04:26.61,0:04:31.21,Default,,0000,0000,0000,,armadillo, it's still alive, and it\Nweighs, let's say, ten kilograms. The
Dialogue: 0,0:04:31.21,0:04:35.50,Default,,0000,0000,0000,,second one is dead, a little bit heavier,\Nweighs twelve kilograms. And the third
Dialogue: 0,0:04:35.50,0:04:40.59,Default,,0000,0000,0000,,animal is a parrot that knows, well, it's\Na pirate's parrot, obviously, and maybe
Dialogue: 0,0:04:40.59,0:04:48.06,Default,,0000,0000,0000,,weighs three kilograms. Ok, so far? Ok. So\Nif you have any question about any of
Dialogue: 0,0:04:48.06,0:04:52.26,Default,,0000,0000,0000,,that, then please ask away. So, what\Nhappens to animals on the Texas Highway
Dialogue: 0,0:04:52.26,0:04:56.54,Default,,0000,0000,0000,,is, you know, people drive cars, they run\Nthem over. So there's a function down
Dialogue: 0,0:04:56.54,0:05:01.10,Default,,0000,0000,0000,,here, and, well, we're doing functional\Nprograming, shouldn't worry you at all.
Dialogue: 0,0:05:01.10,0:05:04.87,Default,,0000,0000,0000,,But what's important here is that it says\Nthere is an animal going in, an animal
Dialogue: 0,0:05:04.87,0:05:09.52,Default,,0000,0000,0000,,going out. And really what this means is\Nthat this animal object up there is not
Dialogue: 0,0:05:09.52,0:05:15.82,Default,,0000,0000,0000,,really the animal. It is the state of the\Nanimal at a given time. So, runOverAnimal.
Dialogue: 0,0:05:15.82,0:05:19.77,Default,,0000,0000,0000,,you can see the type signature that says\Nan animal goes in, an animal goes out. And
Dialogue: 0,0:05:19.77,0:05:24.40,Default,,0000,0000,0000,,what it really means is, the state of the\Nanimal goes in before it gets run over and
Dialogue: 0,0:05:24.40,0:05:29.92,Default,,0000,0000,0000,,the state of the animal after it gets run\Nover comes out. And then while we know
Dialogue: 0,0:05:29.92,0:05:34.26,Default,,0000,0000,0000,,there's two different kinds of animals.\NAnd that means that for the definition of
Dialogue: 0,0:05:34.26,0:05:37.91,Default,,0000,0000,0000,,runOverAnimal, we need what's called\Nequations. There's two different
Dialogue: 0,0:05:37.91,0:05:41.64,Default,,0000,0000,0000,,equations. And the first equation says\Nwhat happens to armadillos when they get
Dialogue: 0,0:05:41.64,0:05:45.84,Default,,0000,0000,0000,,run over. So an armadillo has a liveness\Nand a weight. Here's something going on
Dialogue: 0,0:05:45.84,0:05:50.70,Default,,0000,0000,0000,,called pattern matching. And the second\Nequation says when there's a parrot going
Dialogue: 0,0:05:50.70,0:05:54.69,Default,,0000,0000,0000,,on it has a sentence and a weight, and on\Nthe right hand side, you can see, well,
Dialogue: 0,0:05:54.69,0:05:59.36,Default,,0000,0000,0000,,when an armadillo gets run over. Well, all\Nthat means is, the liveness sort of turns
Dialogue: 0,0:05:59.36,0:06:03.32,Default,,0000,0000,0000,,to Dead. We're constructing a new\Narmadillo object and it's dead and it has
Dialogue: 0,0:06:03.32,0:06:09.21,Default,,0000,0000,0000,,the same weight as before. And the\Nfunction, the equation at the bottom says,
Dialogue: 0,0:06:09.21,0:06:15.18,Default,,0000,0000,0000,,well, when we run over a parrot, it turns\Nreally, really quiet. Ok? So, classic
Dialogue: 0,0:06:15.18,0:06:20.94,Default,,0000,0000,0000,,example. Ok so far. We're going to return\Nto that example at the very end. Right now
Dialogue: 0,0:06:20.94,0:06:24.82,Default,,0000,0000,0000,,it's just to illustrate the language that\Nwe're doing things in and we're going to
Dialogue: 0,0:06:24.82,0:06:32.21,Default,,0000,0000,0000,,do a lot of things without complicated\Nprograms. So, well. So, I'm going to jump
Dialogue: 0,0:06:32.21,0:06:36.02,Default,,0000,0000,0000,,around a little bit. So, one thing. So,\Njust the other day, two weeks ago, I was
Dialogue: 0,0:06:36.02,0:06:40.12,Default,,0000,0000,0000,,teaching a course on architecture and\Nsomebody said: Well, there's this problem.
Dialogue: 0,0:06:40.12,0:06:43.96,Default,,0000,0000,0000,,I'm building a domain model. I'm putting\Nthe domain model in a database. And, you
Dialogue: 0,0:06:43.96,0:06:47.43,Default,,0000,0000,0000,,know, customer comes in, has new\Nrequirement or somebody comes in, has new
Dialogue: 0,0:06:47.43,0:06:51.26,Default,,0000,0000,0000,,requirements. And that always ends the\Nsame way. I put a new call in the database
Dialogue: 0,0:06:51.26,0:06:55.81,Default,,0000,0000,0000,,and, you know, seven, eight, nine, it just\Ngoes on and on. As the software gets older
Dialogue: 0,0:06:55.81,0:07:01.33,Default,,0000,0000,0000,,and older and older, more columns that\Ncreate the old ones seem a little stale.
Dialogue: 0,0:07:01.33,0:07:08.25,Default,,0000,0000,0000,,And so, yes, well, how can we build models\Nthat are flexible? And so, here's
Dialogue: 0,0:07:08.25,0:07:12.95,Default,,0000,0000,0000,,something completely different, you might\Nthink. So, here's sort of the key to that,
Dialogue: 0,0:07:12.95,0:07:16.80,Default,,0000,0000,0000,,to building flexible models. Does anybody\Nrecognize this? Does anybody associate a
Dialogue: 0,0:07:16.80,0:07:23.02,Default,,0000,0000,0000,,word with this? {\i1}laughter{\i0} Very good. So,\Nyou might remember, depending on what
Dialogue: 0,0:07:23.02,0:07:26.81,Default,,0000,0000,0000,,state you went to school in, you might\Nremember that this is a property called
Dialogue: 0,0:07:26.81,0:07:31.91,Default,,0000,0000,0000,,associativity. Right? And it means that we\Ncan associate either the A and the B first
Dialogue: 0,0:07:31.91,0:07:38.20,Default,,0000,0000,0000,,with the parentheses or the B and the C.\NSo, and this is, if you take away one
Dialogue: 0,0:07:38.20,0:07:42.86,Default,,0000,0000,0000,,thing from this talk, it's associativity.\NKnowing what that is is one of the most
Dialogue: 0,0:07:42.86,0:07:47.06,Default,,0000,0000,0000,,useful things in software development. So,\Nof course it's just a generic equation, we
Dialogue: 0,0:07:47.06,0:07:51.02,Default,,0000,0000,0000,,really need to be more specific, namely\Nthat we're dealing with numbers and
Dialogue: 0,0:07:51.02,0:07:54.88,Default,,0000,0000,0000,,addition. And you might know that it's not\Njust addition that's associative. Also,
Dialogue: 0,0:07:54.88,0:07:58.67,Default,,0000,0000,0000,,multiplication, for example, is\Nassociative. So here's a little mathy
Dialogue: 0,0:07:58.67,0:08:03.76,Default,,0000,0000,0000,,stuff there at the beginning. So, you see\Nthat upside down A. That says "for all".
Dialogue: 0,0:08:03.76,0:08:09.03,Default,,0000,0000,0000,,We just say for all. What that means is\N"for all A, B and C". And then, this funny
Dialogue: 0,0:08:09.03,0:08:13.85,Default,,0000,0000,0000,,epsilon-shape letter kind of thing, it\Nmeans "element of". And then that funky N
Dialogue: 0,0:08:13.85,0:08:17.49,Default,,0000,0000,0000,,means the natural numbers. So all the\Nnumbers from zero, one, two, three, the
Dialogue: 0,0:08:17.49,0:08:22.79,Default,,0000,0000,0000,,whole numbers from zero on up. So, what\Nthat means is, for all natural numbers A,
Dialogue: 0,0:08:22.79,0:08:29.72,Default,,0000,0000,0000,,B and C, the associative property holds\Nwhen you add them up. But while it says
Dialogue: 0,0:08:29.72,0:08:33.50,Default,,0000,0000,0000,,numbers in addition, it doesn't just hold\Nfor numbers and, addition, in fact,
Dialogue: 0,0:08:33.50,0:08:37.82,Default,,0000,0000,0000,,associativity is everywhere around us.\NSpecifically, it's everywhere around us
Dialogue: 0,0:08:37.82,0:08:41.68,Default,,0000,0000,0000,,when we program. So here's another\Nexample. When you're dealing with lists
Dialogue: 0,0:08:41.68,0:08:45.10,Default,,0000,0000,0000,,and that funky, the two pluses that you\Nsee there, they are just list
Dialogue: 0,0:08:45.10,0:08:50.45,Default,,0000,0000,0000,,concatenation. So you concatenate two\Nlists and well, of course you can
Dialogue: 0,0:08:50.45,0:08:55.81,Default,,0000,0000,0000,,concatenate three lists by just using that\Ndouble plus in any order. And that's also
Dialogue: 0,0:08:55.81,0:09:00.73,Default,,0000,0000,0000,,associative. So, it doesn't matter if you\Nfirst concatenate the B and the C and then
Dialogue: 0,0:09:00.73,0:09:06.03,Default,,0000,0000,0000,,tack the A onto the front, or if you\Nconcatenate the A and B and tack the C on
Dialogue: 0,0:09:06.03,0:09:09.75,Default,,0000,0000,0000,,at the end. Doesn't matter, you always get\Nthe same result. So lists and
Dialogue: 0,0:09:09.75,0:09:17.25,Default,,0000,0000,0000,,concatenation also have this associative\Nproperty. And here's something that I
Dialogue: 0,0:09:17.25,0:09:22.14,Default,,0000,0000,0000,,always find very, very enlightening is\Nthat you can construct images that way.
Dialogue: 0,0:09:22.14,0:09:27.47,Default,,0000,0000,0000,,Well, you don't see it here. So here's an\Nimage. Well, it's from a cool researcher
Dialogue: 0,0:09:27.47,0:09:31.61,Default,,0000,0000,0000,,of mine and functional programing, Brent\NYorgey, and he has a great library out
Dialogue: 0,0:09:31.61,0:09:37.02,Default,,0000,0000,0000,,called diagrams, for constructing diagrams\Nout of parts. And so this really is what
Dialogue: 0,0:09:37.02,0:09:40.84,Default,,0000,0000,0000,,associativity is about. It's about\Noperators that construct things out of
Dialogue: 0,0:09:40.84,0:09:44.74,Default,,0000,0000,0000,,parts. And so, as you can see here, well\Nthere's different shapes here, there's
Dialogue: 0,0:09:44.74,0:09:48.50,Default,,0000,0000,0000,,sort of the black rectangles, there's a\Ndifferent rectangle set, that denote the
Dialogue: 0,0:09:48.50,0:09:52.18,Default,,0000,0000,0000,,towers of Hanoi. We're not really going to\Ndeal with the towers of Hanoi here,
Dialogue: 0,0:09:52.18,0:09:57.99,Default,,0000,0000,0000,,really. The important thing that the image\Nconsists of several parts. And well, in
Dialogue: 0,0:09:57.99,0:10:01.30,Default,,0000,0000,0000,,normal or sort of in classic object-\Noriented programming, when you do
Dialogue: 0,0:10:01.30,0:10:05.64,Default,,0000,0000,0000,,graphics, you have a canvas and you might\Ndraw pixels on that canvas. You know,
Dialogue: 0,0:10:05.64,0:10:11.17,Default,,0000,0000,0000,,might be square shaped or a circle shaped\Ncanvas pixels. But what we're doing here
Dialogue: 0,0:10:11.17,0:10:18.08,Default,,0000,0000,0000,,is, we are treating an image as a data\Ntype and the definition is not important.
Dialogue: 0,0:10:18.08,0:10:23.35,Default,,0000,0000,0000,,What is important is that there are a\Ncouple of functions that construct sort of
Dialogue: 0,0:10:23.35,0:10:28.67,Default,,0000,0000,0000,,simple images. So here's a function that\Nyou might imagine called star and it
Dialogue: 0,0:10:28.67,0:10:33.79,Default,,0000,0000,0000,,constructs stars. And well, you can see up\Nthere there's a type declaration and it
Dialogue: 0,0:10:33.79,0:10:37.95,Default,,0000,0000,0000,,says, well, the star function, it accepts\Nan integer, it accepts a Mode, whatever
Dialogue: 0,0:10:37.95,0:10:42.21,Default,,0000,0000,0000,,that is, accepts a Color and it produces\Nan Image. And we can call that star
Dialogue: 0,0:10:42.21,0:10:48.75,Default,,0000,0000,0000,,function with the arguments 200 and Solid\Nand Gold. So Mode is Solid or Outline. And
Dialogue: 0,0:10:48.75,0:10:53.98,Default,,0000,0000,0000,,then we have a Color and we get Image and\Nthat image is an object. Not particularly
Dialogue: 0,0:10:53.98,0:11:00.14,Default,,0000,0000,0000,,exciting. But while we might have another\Nfunction called Polygon, Polygon takes two
Dialogue: 0,0:11:00.14,0:11:05.76,Default,,0000,0000,0000,,integers that denote the size of the\Npolygon and the number of vertices, and
Dialogue: 0,0:11:05.76,0:11:09.76,Default,,0000,0000,0000,,also whether it's an outline or whether\Nit's solid and a color. And for example,
Dialogue: 0,0:11:09.76,0:11:17.08,Default,,0000,0000,0000,,if we call it with 180, again, that's the\Nsize and 5 we get a five corner polygon
Dialogue: 0,0:11:17.08,0:11:23.39,Default,,0000,0000,0000,,and we get that as an outline and it's in\Nred. Now, the idea here is that we can
Dialogue: 0,0:11:23.39,0:11:27.49,Default,,0000,0000,0000,,combine. Just as we can combine two\Nnumbers or we can combine two lists, we
Dialogue: 0,0:11:27.49,0:11:31.63,Default,,0000,0000,0000,,can combine two images. Maybe the most\Nintuitive way of combining two images is
Dialogue: 0,0:11:31.63,0:11:36.56,Default,,0000,0000,0000,,just sticking them beside each other. So\Nthere's a function there called beside.
Dialogue: 0,0:11:36.56,0:11:41.01,Default,,0000,0000,0000,,And it takes an image and it takes another\Nimage and produces an image. Right. And
Dialogue: 0,0:11:41.01,0:11:44.82,Default,,0000,0000,0000,,this is exactly what we're thinking about\Nwhen we talk about associativity. We're
Dialogue: 0,0:11:44.82,0:11:50.71,Default,,0000,0000,0000,,talking about a sort of a binary operator\Nthat produces the same thing that went in.
Dialogue: 0,0:11:50.71,0:11:55.64,Default,,0000,0000,0000,,And so, for example, we could stick those\Ntwo images next to each other. We could
Dialogue: 0,0:11:55.64,0:12:01.25,Default,,0000,0000,0000,,also imagine an operator called above that\Njust puts one image above the other image.
Dialogue: 0,0:12:01.25,0:12:05.27,Default,,0000,0000,0000,,And we can combine these two things. Here\Nit really is important that the same thing
Dialogue: 0,0:12:05.27,0:12:09.52,Default,,0000,0000,0000,,comes out so that it's image goes in,\Nanother image goes in, an image goes out.
Dialogue: 0,0:12:09.52,0:12:14.53,Default,,0000,0000,0000,,So we could again call above on the result\Nof beside and make arrangements. So here's
Dialogue: 0,0:12:14.53,0:12:18.83,Default,,0000,0000,0000,,a tiling arrangement for your bathroom or\Nsomething like that. Now, beside and above
Dialogue: 0,0:12:18.83,0:12:23.93,Default,,0000,0000,0000,,are are two possible operators and you\Nmight already think about associativity,
Dialogue: 0,0:12:23.93,0:12:28.99,Default,,0000,0000,0000,,but really the more fundamental one is\Noverlay. You put two images on top of each
Dialogue: 0,0:12:28.99,0:12:33.28,Default,,0000,0000,0000,,other. And so again, overlay has the right\Ntype. An image goes in, another image goes
Dialogue: 0,0:12:33.28,0:12:38.20,Default,,0000,0000,0000,,in, and an image comes out. And if we take\Nthe gold star and the pentagon and put
Dialogue: 0,0:12:38.20,0:12:46.09,Default,,0000,0000,0000,,them on top of each other, then it looks\Nlike this. And we can then formulate an
Dialogue: 0,0:12:46.09,0:12:51.56,Default,,0000,0000,0000,,associativity property. It might not quite\Nlook the same because I wrote overlay in
Dialogue: 0,0:12:51.56,0:12:56.31,Default,,0000,0000,0000,,front rather than between the operators.\NWe could also write it between. But just
Dialogue: 0,0:12:56.31,0:13:00.25,Default,,0000,0000,0000,,to show you that it's the same idea. So,\Nit doesn't really matter if we first take
Dialogue: 0,0:13:00.25,0:13:05.21,Default,,0000,0000,0000,,two images, A and B and superimpose those\Ntwo and then put those two on top of C or
Dialogue: 0,0:13:05.21,0:13:13.32,Default,,0000,0000,0000,,if we do it in another order. Does that\Nmake sense so far? Ok. No? Do you have a
Dialogue: 0,0:13:13.32,0:13:16.39,Default,,0000,0000,0000,,question?\NAnonymous: {\i1}Mumbling{\i0}
Dialogue: 0,0:13:16.39,0:13:20.97,Default,,0000,0000,0000,,Mike: Yeah, so ahh, good point, good\Npoint. So this implies that there must be
Dialogue: 0,0:13:20.97,0:13:24.91,Default,,0000,0000,0000,,some kind of, that there's probably some\Nnotion of transparency involved. Yes. Yes,
Dialogue: 0,0:13:24.91,0:13:29.48,Default,,0000,0000,0000,,there is. But then you have associativity.\NAnd really what it means. Very good
Dialogue: 0,0:13:29.48,0:13:38.40,Default,,0000,0000,0000,,question. So, if you think of this image\Nin terms of the color at certain
Dialogue: 0,0:13:38.40,0:13:43.60,Default,,0000,0000,0000,,coordinates, Right, Well, you need to\Nthink about how to combine those two
Dialogue: 0,0:13:43.60,0:13:48.67,Default,,0000,0000,0000,,colors that are in the constituent images.\NAnd you can imagine that there also has to
Dialogue: 0,0:13:48.67,0:13:53.33,Default,,0000,0000,0000,,be a combination operation for the colour.\NAnd that also needs to be associative as a
Dialogue: 0,0:13:53.33,0:13:58.60,Default,,0000,0000,0000,,prerequisite for the for the overlay\Noperation to be associative. Does that
Dialogue: 0,0:13:58.60,0:14:07.67,Default,,0000,0000,0000,,make sense now? Thank you. Good question.\NGreat question. So anyway, so since this
Dialogue: 0,0:14:07.67,0:14:11.59,Default,,0000,0000,0000,,associativity property is something that\Nis not just restricted to numbers, as we
Dialogue: 0,0:14:11.59,0:14:15.23,Default,,0000,0000,0000,,may have learned in school, it really\Nmakes sense to get. And that means that
Dialogue: 0,0:14:15.23,0:14:18.98,Default,,0000,0000,0000,,when we talk about associativity, we\Nalways have to name two things. We have to
Dialogue: 0,0:14:18.98,0:14:22.68,Default,,0000,0000,0000,,say what set we're operating on and what\Nthe operation is. And the combination
Dialogue: 0,0:14:22.68,0:14:28.37,Default,,0000,0000,0000,,those two things has a name in mathematics\Nand it's not the best name, but it's
Dialogue: 0,0:14:28.37,0:14:34.04,Default,,0000,0000,0000,,called a semigroup. Right. And, but, you\Nknow, if you drop it in certain circles,
Dialogue: 0,0:14:34.04,0:14:39.10,Default,,0000,0000,0000,,they'll think that you're an expert on\Nmathematics, you might try that. So, just
Dialogue: 0,0:14:39.10,0:14:43.03,Default,,0000,0000,0000,,to go over that: So, you have some subset\NS, and that S might be Image, it might be
Dialogue: 0,0:14:43.03,0:14:46.64,Default,,0000,0000,0000,,the natural numbers or something like\Nthat. And we have an operation that I'm
Dialogue: 0,0:14:46.64,0:14:53.57,Default,,0000,0000,0000,,just gonna call circle here, then take any\Na, b and c from that set S. We can use
Dialogue: 0,0:14:53.57,0:14:57.77,Default,,0000,0000,0000,,circle as an operator and we have that\Nassociativity property and for that circle
Dialogue: 0,0:14:57.77,0:15:02.39,Default,,0000,0000,0000,,you can put in overlay, you can put in\Nbeside, you can put in above, you can put
Dialogue: 0,0:15:02.39,0:15:08.90,Default,,0000,0000,0000,,in + you can put in times or you can put\Nin the list concatenation operator, the
Dialogue: 0,0:15:08.90,0:15:15.76,Default,,0000,0000,0000,,++. Okay? And that associativity is great.\NIt's really my favorite property because
Dialogue: 0,0:15:15.76,0:15:20.12,Default,,0000,0000,0000,,it means when we have a whole lot of\Nthings that we combine, we can
Dialogue: 0,0:15:20.12,0:15:24.56,Default,,0000,0000,0000,,parenthesise in any way we want. We will\Nget the same result no matter which way we
Dialogue: 0,0:15:24.56,0:15:28.84,Default,,0000,0000,0000,,parenthesise them. And that really means,\Nwe can leave out the parentheses when we
Dialogue: 0,0:15:28.84,0:15:33.07,Default,,0000,0000,0000,,write an expression that involves only the\Ncircle operator if it's associative, if we
Dialogue: 0,0:15:33.07,0:15:36.84,Default,,0000,0000,0000,,can just leave out all the parentheses\Nbecause the parentheses don't matter. And
Dialogue: 0,0:15:36.84,0:15:41.89,Default,,0000,0000,0000,,that makes it well, that makes it\Ninstantly easier to read, I think. Also it
Dialogue: 0,0:15:41.89,0:15:46.87,Default,,0000,0000,0000,,has practical uses. So if you do big data\Nprocessing associativity means that if you
Dialogue: 0,0:15:46.87,0:15:52.04,Default,,0000,0000,0000,,have large datasets that span several\Nmachines or several hard drives or several
Dialogue: 0,0:15:52.04,0:15:58.68,Default,,0000,0000,0000,,data sources, and you're combining them\Nand you have an associative combination
Dialogue: 0,0:15:58.68,0:16:03.26,Default,,0000,0000,0000,,operation, it just means you can rearrange\Nthat combination operation according to
Dialogue: 0,0:16:03.26,0:16:07.58,Default,,0000,0000,0000,,the load in your compute cluster. And that\Nmakes it a very useful property when
Dialogue: 0,0:16:07.58,0:16:12.22,Default,,0000,0000,0000,,you're doing big data processing in sort\Nof MapReduce based frameworks. But, I
Dialogue: 0,0:16:12.22,0:16:16.41,Default,,0000,0000,0000,,mean, that's a practical application, but\NI think it's much more useful,
Dialogue: 0,0:16:16.41,0:16:21.22,Default,,0000,0000,0000,,associativity is much more useful when you\Nuse it for designing your domain model.
Dialogue: 0,0:16:21.22,0:16:25.75,Default,,0000,0000,0000,,And I talked in the beginning how, well,\Nyou want to avoid always adding more
Dialogue: 0,0:16:25.75,0:16:29.56,Default,,0000,0000,0000,,database columns. And one way of doing\Nthat is to view your domain model, not as
Dialogue: 0,0:16:29.56,0:16:33.22,Default,,0000,0000,0000,,something that has more and more\Nproperties, but your domain model as
Dialogue: 0,0:16:33.22,0:16:37.44,Default,,0000,0000,0000,,building blocks that you combine into a\Nlarger building blocks the same way that
Dialogue: 0,0:16:37.44,0:16:42.75,Default,,0000,0000,0000,,we combine images from simpler images. So\Nhere's one of the great papers from
Dialogue: 0,0:16:42.75,0:16:46.44,Default,,0000,0000,0000,,functional programing, one of my two or\Nthree favorites from Brent Yorgey. And
Dialogue: 0,0:16:46.44,0:16:50.22,Default,,0000,0000,0000,,it's called "Something Something: Theme\Nand Variations". And you can see that it
Dialogue: 0,0:16:50.22,0:16:54.94,Default,,0000,0000,0000,,is about images. And these images get\Nsuperimposed with an operation that is
Dialogue: 0,0:16:54.94,0:17:00.59,Default,,0000,0000,0000,,just like overlay and that is, that title\Nis eminently googleable. Now, it has a
Dialogue: 0,0:17:00.59,0:17:04.54,Default,,0000,0000,0000,,funny word there. It says, it doesn't say\Nsemigroup, could say"Semigroup: Theme and
Dialogue: 0,0:17:04.54,0:17:08.64,Default,,0000,0000,0000,,Variation", it says "Monoid: Theme and\NVariation". And a monoid, well, it's also
Dialogue: 0,0:17:08.64,0:17:12.36,Default,,0000,0000,0000,,not something, even though it sounds kind\Nof fancy, it's actually not much more
Dialogue: 0,0:17:12.36,0:17:16.40,Default,,0000,0000,0000,,complicated than a semigroup. It's a\Nsemigroup. And also the semigroup has a
Dialogue: 0,0:17:16.40,0:17:20.19,Default,,0000,0000,0000,,special element called the neutral\Nelement. And whenever we combine something
Dialogue: 0,0:17:20.19,0:17:24.07,Default,,0000,0000,0000,,with a neutral element, it doesn't matter\Nif we do it in front or at the back, we
Dialogue: 0,0:17:24.07,0:17:27.79,Default,,0000,0000,0000,,get the same thing back. So, of course,\Nthe neutral element with respect to
Dialogue: 0,0:17:27.79,0:17:33.66,Default,,0000,0000,0000,,numbers, in addition, would be zero. The\Nneutral element with respect to lists and
Dialogue: 0,0:17:33.66,0:17:38.54,Default,,0000,0000,0000,,and concatenation would be the empty list.\NI always hear several voices. That's
Dialogue: 0,0:17:38.54,0:17:42.50,Default,,0000,0000,0000,,wonderful. Thank you. And the same thing\Nfor the overlay and beside and above, you
Dialogue: 0,0:17:42.50,0:17:46.40,Default,,0000,0000,0000,,can imagine that you have just an empty\Nimage that has only, that consists only of
Dialogue: 0,0:17:46.40,0:17:51.53,Default,,0000,0000,0000,,transparency, that can work as the neutral\Nelement. So all of these things that I
Dialogue: 0,0:17:51.53,0:17:55.31,Default,,0000,0000,0000,,showed you that are associative, they're\Nnot just associative. They're not just
Dialogue: 0,0:17:55.31,0:18:00.74,Default,,0000,0000,0000,,semigroups, they're also monoids. And so,\Nas I said, as long as you remember
Dialogue: 0,0:18:00.74,0:18:04.51,Default,,0000,0000,0000,,associativity, that's the important thing.\NBut often you also find a monoid, and
Dialogue: 0,0:18:04.51,0:18:07.91,Default,,0000,0000,0000,,monoids in the wild they're just\Neverywhere. We've seen them for numbers
Dialogue: 0,0:18:07.91,0:18:12.50,Default,,0000,0000,0000,,and lists and images, music forms a\Nnatural monoid. You can you can describe
Dialogue: 0,0:18:12.50,0:18:19.66,Default,,0000,0000,0000,,musical structure with monoid operations.\NYou can treat animations, the time axis.
Dialogue: 0,0:18:19.66,0:18:24.67,Default,,0000,0000,0000,,You can define monoidal combination of\Nanimations. A famous example in functional
Dialogue: 0,0:18:24.67,0:18:28.63,Default,,0000,0000,0000,,programming is with financial contracts.\NIf you were here last year for a talk of
Dialogue: 0,0:18:28.63,0:18:32.27,Default,,0000,0000,0000,,mine, we talked about semiconductor-\Nfabrication routes, which sounds very
Dialogue: 0,0:18:32.27,0:18:37.12,Default,,0000,0000,0000,,concrete, but also they form a monoid. The\Nproperties themselves that we'll see for a
Dialogue: 0,0:18:37.12,0:18:40.69,Default,,0000,0000,0000,,monoid are all kinds of things. They're\Neverywhere around you. And these are
Dialogue: 0,0:18:40.69,0:18:44.82,Default,,0000,0000,0000,,really the key towards making flexible\Ndomain models because in almost any domain
Dialogue: 0,0:18:44.82,0:18:48.88,Default,,0000,0000,0000,,model you can find a monoid just by\Nlooking for building blocks and for ways
Dialogue: 0,0:18:48.88,0:18:54.33,Default,,0000,0000,0000,,of combining those building blocks into a\Nlarger building blocks. So let me get
Dialogue: 0,0:18:54.33,0:19:00.10,Default,,0000,0000,0000,,back. So I said, well, you can use\Nassociativity or you can use this monoid
Dialogue: 0,0:19:00.10,0:19:04.26,Default,,0000,0000,0000,,thing to guide your design. And I haven't\Nreally made that concrete yet. And so I
Dialogue: 0,0:19:04.26,0:19:09.37,Default,,0000,0000,0000,,stole a couple of pictures from Brent's\Npaper. So you remember the beside and the
Dialogue: 0,0:19:09.37,0:19:14.38,Default,,0000,0000,0000,,above operations. And those are fine for\Narranging things sort of in the vertical
Dialogue: 0,0:19:14.38,0:19:19.90,Default,,0000,0000,0000,,and the horizontal axis. The way that they\Nwork is, they make, they put a bounding
Dialogue: 0,0:19:19.90,0:19:23.93,Default,,0000,0000,0000,,box around every picture and then they\Narrange the bounding boxes either beside
Dialogue: 0,0:19:23.93,0:19:28.29,Default,,0000,0000,0000,,each other or above each other. So it's a\Nslightly more involved thought. And that
Dialogue: 0,0:19:28.29,0:19:32.20,Default,,0000,0000,0000,,works great when you're, when, you know,\Nyour picture is, happens to be a square
Dialogue: 0,0:19:32.20,0:19:36.67,Default,,0000,0000,0000,,that's aligned with the axes. It doesn't\Nwork so well if your picture is rotated,
Dialogue: 0,0:19:36.67,0:19:40.30,Default,,0000,0000,0000,,right. Because the bounding box, the\Nbounding box then is too big. And if you
Dialogue: 0,0:19:40.30,0:19:44.26,Default,,0000,0000,0000,,want to attach anything about, just about\Nin any direction, then there's going to be
Dialogue: 0,0:19:44.26,0:19:49.86,Default,,0000,0000,0000,,a gap in your picture. And so beside and\Nabove are not particularly good operations
Dialogue: 0,0:19:49.86,0:19:54.79,Default,,0000,0000,0000,,as the basis for an image library. The\Noverlay operation is much better. But that
Dialogue: 0,0:19:54.79,0:19:59.10,Default,,0000,0000,0000,,leaves open the question how you can\Narrange pictures, several pictures so that
Dialogue: 0,0:19:59.10,0:20:04.94,Default,,0000,0000,0000,,they are beside each other or that they\Njust touch. And Brent came up with this
Dialogue: 0,0:20:04.94,0:20:12.01,Default,,0000,0000,0000,,idea of an envelope, technical idea. So\Nthe idea is that, well, if you give me, so
Dialogue: 0,0:20:12.01,0:20:17.52,Default,,0000,0000,0000,,the red dot there, that's the origin. If\Nyou give me a vector starting at the
Dialogue: 0,0:20:17.52,0:20:22.58,Default,,0000,0000,0000,,origin, I will tell you how far you have\Nto go along that vector so that I can draw
Dialogue: 0,0:20:22.58,0:20:27.47,Default,,0000,0000,0000,,that blue perpendicular line that's just\Noutside the shape. And that's called an
Dialogue: 0,0:20:27.47,0:20:33.96,Default,,0000,0000,0000,,envelope. And envelopes are wonderful. So\Nif you ship each picture not just with
Dialogue: 0,0:20:33.96,0:20:38.40,Default,,0000,0000,0000,,sort of the visuals that you see, but also\Nwith a function that describes the
Dialogue: 0,0:20:38.40,0:20:43.68,Default,,0000,0000,0000,,envelope, then you can use that envelope\Nto arrange pictures both in the horizontal
Dialogue: 0,0:20:43.68,0:20:48.47,Default,,0000,0000,0000,,and the vertical, but also in the diagonal\Nby just drawing vectors so that they
Dialogue: 0,0:20:48.47,0:20:52.58,Default,,0000,0000,0000,,touch. So, that's a slightly more\Ncomplicated idea. Does it make sense? And
Dialogue: 0,0:20:52.58,0:20:57.16,Default,,0000,0000,0000,,Brent goes through the motions of using\Nthat inspiration from the monoid that he
Dialogue: 0,0:20:57.16,0:21:02.81,Default,,0000,0000,0000,,is getting. He's saying "Everything must\Nbe a monoid! Absolutely.", and uses that
Dialogue: 0,0:21:02.81,0:21:06.17,Default,,0000,0000,0000,,as a guiding principle through the\Nlibrary. So I'm not going to go into
Dialogue: 0,0:21:06.17,0:21:11.38,Default,,0000,0000,0000,,technical detail on how that works, but\Nit's a very pleasing paper to read on
Dialogue: 0,0:21:11.38,0:21:17.56,Default,,0000,0000,0000,,that. And it results in a beautiful\Nlibrary that's great fun to use. So that
Dialogue: 0,0:21:17.56,0:21:22.05,Default,,0000,0000,0000,,means, though, that you also have to find\Na monoidal combination operation for the
Dialogue: 0,0:21:22.05,0:21:25.67,Default,,0000,0000,0000,,envelopes. You can't just, we've already\Nseen how we can combine the pictures
Dialogue: 0,0:21:25.67,0:21:29.35,Default,,0000,0000,0000,,themselves, but we also need to combine\Nthe envelopes. And fortunately, that's
Dialogue: 0,0:21:29.35,0:21:33.30,Default,,0000,0000,0000,,pretty easy. If somebody sets a vector in\Na certain direction, then that envelope is
Dialogue: 0,0:21:33.30,0:21:37.04,Default,,0000,0000,0000,,just a maximum. Those two pictures, right,\Nif you combine that ellipse and that
Dialogue: 0,0:21:37.04,0:21:41.26,Default,,0000,0000,0000,,square, you can see that I'm just going to\Nhave to go to the maximum of those two
Dialogue: 0,0:21:41.26,0:21:46.70,Default,,0000,0000,0000,,numbers in order to just be outside the\Ncomposite shape that that comes up
Dialogue: 0,0:21:46.70,0:21:52.93,Default,,0000,0000,0000,,superimposing those two things. So that's\Ngreat. Now, I sort of introduced these
Dialogue: 0,0:21:52.93,0:21:56.92,Default,,0000,0000,0000,,properties as a mathematical thing, right.\NI said, well, there's this fancy, fancy
Dialogue: 0,0:21:56.92,0:22:02.83,Default,,0000,0000,0000,,upside down operator says for all images\Nand we might say for all images. Now, we
Dialogue: 0,0:22:02.83,0:22:08.81,Default,,0000,0000,0000,,can also formulate these properties as\Ncode. And that's really where additional
Dialogue: 0,0:22:08.81,0:22:12.24,Default,,0000,0000,0000,,magic is. So, for example, the\Nassociativity property, well, there's not
Dialogue: 0,0:22:12.24,0:22:15.61,Default,,0000,0000,0000,,much of a difference except that the\Nimage1 and image2, they are now in
Dialogue: 0,0:22:15.61,0:22:19.64,Default,,0000,0000,0000,,typewriter font. So we could put those in\Nthe program. But there's still that
Dialogue: 0,0:22:19.64,0:22:24.13,Default,,0000,0000,0000,,mathematical stuff on top. But in a\Nfunctional language, in a lot of other
Dialogue: 0,0:22:24.13,0:22:28.34,Default,,0000,0000,0000,,languages too by now, we could also put\Nthe top line and translate that into code.
Dialogue: 0,0:22:28.34,0:22:32.19,Default,,0000,0000,0000,,And it might look like this. So that's\Nwhat it looks like in Idris. So, it's not
Dialogue: 0,0:22:32.19,0:22:37.38,Default,,0000,0000,0000,,quite the same, but maybe we recognize the\Nstructure. So, we say, well, there's a
Dialogue: 0,0:22:37.38,0:22:41.37,Default,,0000,0000,0000,,property called and the property is just\Ncalled overlayAssociative. So we give it a
Dialogue: 0,0:22:41.37,0:22:48.10,Default,,0000,0000,0000,,name. So, Idris is an ASCII language,\Nstill so, primarily. So, we say just
Dialogue: 0,0:22:48.10,0:22:52.76,Default,,0000,0000,0000,,forAll there instead of the upside down\Nall. And then it says arbTriple arbImage
Dialogue: 0,0:22:52.76,0:22:58.93,Default,,0000,0000,0000,,arbImage arbImage. And that means for all\Narbitrary triples of arbitrary images and
Dialogue: 0,0:22:58.93,0:23:02.18,Default,,0000,0000,0000,,other arbitrary image and another\Narbitrary image, so, triples, three
Dialogue: 0,0:23:02.18,0:23:08.43,Default,,0000,0000,0000,,things. And we're going to call those\Nthree images image1, image2 and image3.
Dialogue: 0,0:23:08.43,0:23:15.15,Default,,0000,0000,0000,,That funky backslash there, that's a\NLambda in Idris. And then the overlay prop
Dialogue: 0,0:23:15.15,0:23:21.46,Default,,0000,0000,0000,,means that while, if we overlay one way\Nand we overlay another way, according to
Dialogue: 0,0:23:21.46,0:23:26.26,Default,,0000,0000,0000,,associativity, we get the same result. Do\Nyou recognize that structure? Right. That
Dialogue: 0,0:23:26.26,0:23:31.06,Default,,0000,0000,0000,,it's the same thing. So that we're writing\Nstructurally the same thing that we wrote
Dialogue: 0,0:23:31.06,0:23:36.79,Default,,0000,0000,0000,,in mathematical notation. Now as a piece\Nof code. And now the great thing is once
Dialogue: 0,0:23:36.79,0:23:40.80,Default,,0000,0000,0000,,we've written it as a piece of code, we\Ncan manipulate it in a program.
Dialogue: 0,0:23:40.80,0:23:44.57,Default,,0000,0000,0000,,So, one way, there is different ways\Nof manipulating it. But one of the most
Dialogue: 0,0:23:44.57,0:23:48.14,Default,,0000,0000,0000,,useful ones is, again by another great\Nresearcher in functional programming,
Dialogue: 0,0:23:48.14,0:23:52.00,Default,,0000,0000,0000,,John Hughes, came up with something called\NQuickCheck. So if there's another thing
Dialogue: 0,0:23:52.00,0:23:55.87,Default,,0000,0000,0000,,you take away from this talk is: google\NQuickCheck. And whatever language you use,
Dialogue: 0,0:23:55.87,0:24:00.53,Default,,0000,0000,0000,,it doesn't have to be Idris. In fact, I\Nhad to hack together a QuickCheck for this
Dialogue: 0,0:24:00.53,0:24:04.40,Default,,0000,0000,0000,,talk, but basically any other language is\Ngoing to have a QuickCheck, whether that
Dialogue: 0,0:24:04.40,0:24:08.73,Default,,0000,0000,0000,,language be a functional language or\Nwhether it's Java or Python or R or
Dialogue: 0,0:24:08.73,0:24:15.49,Default,,0000,0000,0000,,something like that. You can always get a\NQuickCheck for that. And I'm going to try
Dialogue: 0,0:24:15.49,0:24:22.56,Default,,0000,0000,0000,,and demonstrate this QuickCheck thing not\Nby thinking about the design so much, but
Dialogue: 0,0:24:22.56,0:24:28.09,Default,,0000,0000,0000,,by demonstrating a property of something\Nthat's very error prone. So, here's this
Dialogue: 0,0:24:28.09,0:24:35.23,Default,,0000,0000,0000,,idea, we want to have a representation for\Nsets of natural numbers. And we're going
Dialogue: 0,0:24:35.23,0:24:40.80,Default,,0000,0000,0000,,to represent those sets of natural numbers\Nby a list of intervals. So, by a list of
Dialogue: 0,0:24:40.80,0:24:44.99,Default,,0000,0000,0000,,ranges, if you will, between two numbers.\NNow, I'll try to explain that. So, up
Dialogue: 0,0:24:44.99,0:24:49.51,Default,,0000,0000,0000,,there at the top, it has a type\Ndefinition. It says, ISet, interval set,
Dialogue: 0,0:24:49.51,0:24:56.65,Default,,0000,0000,0000,,is a type. And that type is defined to be\Njust a synonym for a list of pairs of
Dialogue: 0,0:24:56.65,0:25:00.38,Default,,0000,0000,0000,,natural numbers. That's what those round\Nparentheses with a comma in the middle
Dialogue: 0,0:25:00.38,0:25:05.34,Default,,0000,0000,0000,,mean. OK. And just to see what that means\Nis, there's a function there. I haven't,
Dialogue: 0,0:25:05.34,0:25:10.00,Default,,0000,0000,0000,,I've lighted the definition, but what's\Nimportant about it is its type signature.
Dialogue: 0,0:25:10.00,0:25:15.61,Default,,0000,0000,0000,,It takes an interval set and it produces a\Nlist of all of the members of that set.
Dialogue: 0,0:25:15.61,0:25:20.92,Default,,0000,0000,0000,,And you can see sort of a demo thing here\Nthat I typed in before the talk. So, if I
Dialogue: 0,0:25:20.92,0:25:27.26,Default,,0000,0000,0000,,apply iToList so that, the brackets there\Nthey just mean the list, and we feed in a
Dialogue: 0,0:25:27.26,0:25:32.24,Default,,0000,0000,0000,,list of intervals and those intervals are\Nfrom zero to three, from five to seven,
Dialogue: 0,0:25:32.24,0:25:36.86,Default,,0000,0000,0000,,and from nine to ten, respectively.\NThey're all inclusive. And you can see
Dialogue: 0,0:25:36.86,0:25:40.46,Default,,0000,0000,0000,,down there is a list of all of the\Nmembers. So, the first interval is from 0
Dialogue: 0,0:25:40.46,0:25:47.04,Default,,0000,0000,0000,,to 3. So, it has the numbers 0, 1, 2 and\N3. The next one goes from five to seven.
Dialogue: 0,0:25:47.04,0:25:51.49,Default,,0000,0000,0000,,So it has the three numbers 5, 6, 7. And\Nthe last one goes from nine to ten. So it
Dialogue: 0,0:25:51.49,0:25:56.58,Default,,0000,0000,0000,,has the two numbers, 9 and 10 there. Does\Nthat make any sense again? Slightly more
Dialogue: 0,0:25:56.58,0:26:05.76,Default,,0000,0000,0000,,complicated example. So let's see. So, of\Ncourse, well, not of course, but the way
Dialogue: 0,0:26:05.76,0:26:09.52,Default,,0000,0000,0000,,we want to do it, the way I want to do it\Nis, I want to have the interval set
Dialogue: 0,0:26:09.52,0:26:15.87,Default,,0000,0000,0000,,structured in a certain way. I don't just\Nwant {\i1}any{\i0} list of any pair of numbers to
Dialogue: 0,0:26:15.87,0:26:19.66,Default,,0000,0000,0000,,denote an interval set. And therefore,\Nhere is a function that describes what it
Dialogue: 0,0:26:19.66,0:26:25.61,Default,,0000,0000,0000,,needs to be a valid interval set. Right.\NSo, for example, we don't really, in order
Dialogue: 0,0:26:25.61,0:26:29.43,Default,,0000,0000,0000,,to have efficient processing, we don't\Nreally want two intervals in one interval
Dialogue: 0,0:26:29.43,0:26:33.12,Default,,0000,0000,0000,,set to overlap. Right. We want them to be\Ndisjoint and we also want them to be
Dialogue: 0,0:26:33.12,0:26:37.62,Default,,0000,0000,0000,,ordered so we can have efficient\Noperations for certain things. Right. And
Dialogue: 0,0:26:37.62,0:26:41.41,Default,,0000,0000,0000,,so, let's go through this. So, there is an\NisValid function that just tells you
Dialogue: 0,0:26:41.41,0:26:46.23,Default,,0000,0000,0000,,whether that interval set is valid or not.\NIt says, well, if that set, and there's
Dialogue: 0,0:26:46.23,0:26:50.14,Default,,0000,0000,0000,,three different cases here, which is why\Nthere's three different equations, in the
Dialogue: 0,0:26:50.14,0:26:54.66,Default,,0000,0000,0000,,first equation says the empty interval\Nset, the empty brackets mean the empty
Dialogue: 0,0:26:54.66,0:26:58.75,Default,,0000,0000,0000,,list, and if the intervals, the list\Nrepresenting the interval set is empty,
Dialogue: 0,0:26:58.75,0:27:04.07,Default,,0000,0000,0000,,then we're going to say True. Empty set -\Nperfectly fine. The next case says, our
Dialogue: 0,0:27:04.07,0:27:08.52,Default,,0000,0000,0000,,interval set consists only of a single\Ninterval and that single interval goes
Dialogue: 0,0:27:08.52,0:27:14.21,Default,,0000,0000,0000,,from low to high. Well, we kind of\Ninterpret that there, but, and, well, that
Dialogue: 0,0:27:14.21,0:27:18.36,Default,,0000,0000,0000,,interval set is valid, if low comes in\Nfront of high. Right, they shouldn't be
Dialogue: 0,0:27:18.36,0:27:23.87,Default,,0000,0000,0000,,the other way around. So, does that make\Nsense? Somebody in, can you nod at the
Dialogue: 0,0:27:23.87,0:27:29.01,Default,,0000,0000,0000,,back, a little bit? You're still there?\NOK. Thank you. Great. So, then it becomes
Dialogue: 0,0:27:29.01,0:27:33.19,Default,,0000,0000,0000,,a little bit more complicated and it says,\Nwell, this is the third case, when there's
Dialogue: 0,0:27:33.19,0:27:38.67,Default,,0000,0000,0000,,at least two intervals in the interval\Nset. And those two intervals are, the
Dialogue: 0,0:27:38.67,0:27:44.90,Default,,0000,0000,0000,,first one goes from lo1 to hi1. The second\None goes from lo2 to hi2. So, those ::,
Dialogue: 0,0:27:44.90,0:27:48.81,Default,,0000,0000,0000,,they separate the first element of a list\Nfrom the rest. And then there's the rest
Dialogue: 0,0:27:48.81,0:27:54.14,Default,,0000,0000,0000,,of the list. And it says, well, again, we\Nwant the interval to be ordered so that
Dialogue: 0,0:27:54.14,0:27:59.38,Default,,0000,0000,0000,,the lower numbers are on the left. That's\Nwhere it says lo1 is less or equal hi1.
Dialogue: 0,0:27:59.38,0:28:03.73,Default,,0000,0000,0000,,And then it says, well, that there should\Nbe a gap between two consecutive
Dialogue: 0,0:28:03.73,0:28:09.01,Default,,0000,0000,0000,,intervals. Otherwise, they should be one\Ninterval, which is why the high from one
Dialogue: 0,0:28:09.01,0:28:14.75,Default,,0000,0000,0000,,interval should be separated from the low\Nof the next interval by at least one. And
Dialogue: 0,0:28:14.75,0:28:18.93,Default,,0000,0000,0000,,then we're going to say, well, also we\Nwant all the rest of the list, including
Dialogue: 0,0:28:18.93,0:28:26.74,Default,,0000,0000,0000,,lo2 and hi2 to be valid too. So far so\Ngood? OK, so this is probably, well, the
Dialogue: 0,0:28:26.74,0:28:32.37,Default,,0000,0000,0000,,second most complicated piece of code. So,\Nanyway, so, here's, so, we might imagine a
Dialogue: 0,0:28:32.37,0:28:37.34,Default,,0000,0000,0000,,union function. And the union function,\Nguess what, it forms a monoid, with
Dialogue: 0,0:28:37.34,0:28:43.30,Default,,0000,0000,0000,,respect to interval sets. So, it takes,\Ntwo internal sets go in and another one
Dialogue: 0,0:28:43.30,0:28:47.51,Default,,0000,0000,0000,,comes out. And if you've written that kind\Nof thing before, you might notice it's
Dialogue: 0,0:28:47.51,0:28:52.79,Default,,0000,0000,0000,,probably a little tricky with that fancy\Nvalidity condition that's there. So how
Dialogue: 0,0:28:52.79,0:28:58.25,Default,,0000,0000,0000,,can we get this right? Well, what we do is\Nwe write down properties. Of course, we
Dialogue: 0,0:28:58.25,0:29:02.77,Default,,0000,0000,0000,,could write down associativity. I'll leave\Nthat as an exercise. Another one is just
Dialogue: 0,0:29:02.77,0:29:08.74,Default,,0000,0000,0000,,very simple. Just a very simple property\Nthat says for all pairs of two arbitrary
Dialogue: 0,0:29:08.74,0:29:13.89,Default,,0000,0000,0000,,interval sets, we want the union of those\Ntwo interval sets to be valid, a valid
Dialogue: 0,0:29:13.89,0:29:21.30,Default,,0000,0000,0000,,data structure. We want the union function\Nto preserve validity. OK? Makes sense? So
Dialogue: 0,0:29:21.30,0:29:26.58,Default,,0000,0000,0000,,here's another property that says, well, I\Nalready gave you this function or I told
Dialogue: 0,0:29:26.58,0:29:32.71,Default,,0000,0000,0000,,you that there is this function iToList,\Nwhich just gives us a list of elements of
Dialogue: 0,0:29:32.71,0:29:36.86,Default,,0000,0000,0000,,an interval set. And what we can do is, we\Ncan use sort of that representation,
Dialogue: 0,0:29:36.86,0:29:40.71,Default,,0000,0000,0000,,that's also a representation for sets. We\Ncan use that representation sort of as a
Dialogue: 0,0:29:40.71,0:29:44.64,Default,,0000,0000,0000,,model and say, well, if we take the\Nunions, you see there for all pairs,
Dialogue: 0,0:29:44.64,0:29:49.77,Default,,0000,0000,0000,,again, of arbitrary interval sets, we take\Nthe union. It says iUnion, iset1 and
Dialogue: 0,0:29:49.77,0:29:55.57,Default,,0000,0000,0000,,iset2. And we convert that to a list. And,\Nwe could also do, we could instead convert
Dialogue: 0,0:29:55.57,0:30:00.76,Default,,0000,0000,0000,,each individual set to a list and then\Njust merge those two lists. And that
Dialogue: 0,0:30:00.76,0:30:06.39,Default,,0000,0000,0000,,should yield the same result. So, in a\Nway, we're just giving a very simple model
Dialogue: 0,0:30:06.39,0:30:10.33,Default,,0000,0000,0000,,for our interval sets, right, and that\Nwould, so those two criteria would be kind
Dialogue: 0,0:30:10.33,0:30:15.94,Default,,0000,0000,0000,,of nice to have in order to get our\Nimplementation correct. And I already got
Dialogue: 0,0:30:15.94,0:30:20.44,Default,,0000,0000,0000,,started before the talk on this. Looks\Nlike this. No. Doesn't look like this.
Dialogue: 0,0:30:20.44,0:30:29.39,Default,,0000,0000,0000,,We'll get to that later. But like this.\NSo, here's what I came up with. So, you
Dialogue: 0,0:30:29.39,0:30:33.29,Default,,0000,0000,0000,,see there is that, while there's all this\Nother code there, ignore that. But there
Dialogue: 0,0:30:33.29,0:30:36.96,Default,,0000,0000,0000,,is iUnion says ISet -> ISet -> ISet, do\Nyou see that? And then, there's two
Dialogue: 0,0:30:36.96,0:30:41.12,Default,,0000,0000,0000,,equations that say, well, the first set is\Nempty, then I'm just going to give you the
Dialogue: 0,0:30:41.12,0:30:44.62,Default,,0000,0000,0000,,second one. And if the second one is\Nempty, I'm just going to give you the
Dialogue: 0,0:30:44.62,0:30:49.51,Default,,0000,0000,0000,,first one. Right? Classic things when you\Nhave union or concatenation operations or
Dialogue: 0,0:30:49.51,0:30:54.20,Default,,0000,0000,0000,,something like that. And now you can see\Nthe third case. It gets tricky, right?
Dialogue: 0,0:30:54.20,0:30:58.35,Default,,0000,0000,0000,,Again, you don't need, I mean, main thing\Nis you need to understand it's tricky.
Dialogue: 0,0:30:58.35,0:31:05.84,Default,,0000,0000,0000,,Well, the third one is such that, well,\Nsays so that both have at least one
Dialogue: 0,0:31:05.84,0:31:11.21,Default,,0000,0000,0000,,element and that element is in the\Ninterval lo1 and hi1 in the first case and
Dialogue: 0,0:31:11.21,0:31:15.13,Default,,0000,0000,0000,,lo2 and hi2 in the second case. And then\Nthere's the rest. And I already put in a
Dialogue: 0,0:31:15.13,0:31:20.57,Default,,0000,0000,0000,,little bit of code, and I said, well if\Nlo1 comes after hi1 (means hi2), then we
Dialogue: 0,0:31:20.57,0:31:25.35,Default,,0000,0000,0000,,want to start with lo2 to hi2 and then\Ncontinue with the union. In the other
Dialogue: 0,0:31:25.35,0:31:29.35,Default,,0000,0000,0000,,case, if lo2 comes after hi2 (means hi1),\Nthen we're gonna start with lo1 and hi1.
Dialogue: 0,0:31:29.35,0:31:33.81,Default,,0000,0000,0000,,And in the other case, it means, that no\Ninterval comes before the other, and
Dialogue: 0,0:31:33.81,0:31:38.80,Default,,0000,0000,0000,,therefore we need to merge the two\Nintervals at the beginning. Does that make
Dialogue: 0,0:31:38.80,0:31:43.98,Default,,0000,0000,0000,,remote sense? Right. Don't worry. We'll\Nget back on solid track. So, we just take
Dialogue: 0,0:31:43.98,0:31:47.85,Default,,0000,0000,0000,,the minimum of those two intervals and\Nmaximum of those two intervals and we do
Dialogue: 0,0:31:47.85,0:31:52.09,Default,,0000,0000,0000,,this. Now, the great thing is, I told you\Nabout this tool by John Hughes called
Dialogue: 0,0:31:52.09,0:31:58.74,Default,,0000,0000,0000,,QuickCheck. And the great thing is, we can\Nload this into Idris. And then here comes
Dialogue: 0,0:31:58.74,0:32:10.92,Default,,0000,0000,0000,,a REPL, and we can say, I hope I'm doing\Nthis right. So, we want QuickCheck, and we
Dialogue: 0,0:32:10.92,0:32:16.86,Default,,0000,0000,0000,,want, what was it called? It was called\Nprop_unionCorrect. I hope I'm doing this
Dialogue: 0,0:32:16.86,0:32:21.84,Default,,0000,0000,0000,,right. And, well, very small font. But you\Ncan see here it says "100 tests". And that
Dialogue: 0,0:32:21.84,0:32:27.10,Default,,0000,0000,0000,,is what QuickCheck does, as, it takes your\Ncode version off the property and
Dialogue: 0,0:32:27.10,0:32:32.13,Default,,0000,0000,0000,,automatically generates a lot of tests for\Nthem. And that is super effective at
Dialogue: 0,0:32:32.13,0:32:36.25,Default,,0000,0000,0000,,weeding out bugs. So it says, well, the\Nthing that you wrote is correct. It always
Dialogue: 0,0:32:36.25,0:32:43.55,Default,,0000,0000,0000,,produces interval sets that when you take\Nthe list, it gives you the right result.
Dialogue: 0,0:32:43.55,0:32:50.36,Default,,0000,0000,0000,,But there was that other criterion called\NunionValid. And there it says, and this is
Dialogue: 0,0:32:50.36,0:32:54.52,Default,,0000,0000,0000,,really the better part, of course, of\NQuickCheck is, when it fails, it says it's
Dialogue: 0,0:32:54.52,0:33:00.50,Default,,0000,0000,0000,,falsifiable. It says there is a counter\Nexample. And so, here it says, I did nine
Dialogue: 0,0:33:00.50,0:33:05.07,Default,,0000,0000,0000,,tests, I generated nine random tests, and\NI found one where the result is not valid.
Dialogue: 0,0:33:05.07,0:33:11.36,Default,,0000,0000,0000,,And the great thing is that we can then go\Nand cut and paste this example. So I could
Dialogue: 0,0:33:11.36,0:33:17.81,Default,,0000,0000,0000,,say iUnion, this, remove the comma in the\Nmiddle, and call this. And well, what
Dialogue: 0,0:33:17.81,0:33:23.78,Default,,0000,0000,0000,,happens here is, what we can see is, we\Ncan see 2 and 4, 1 and 1, and 3 and 5, and
Dialogue: 0,0:33:23.78,0:33:27.60,Default,,0000,0000,0000,,what's not valid about. So, by the way,\Nthis is randomized. So, this always goes
Dialogue: 0,0:33:27.60,0:33:31.86,Default,,0000,0000,0000,,differently. So I have to look at it, too.\NSo, then it says, well, those two
Dialogue: 0,0:33:31.86,0:33:35.26,Default,,0000,0000,0000,,intervals, they should really just be\Nmerged and they should just be one
Dialogue: 0,0:33:35.26,0:33:43.71,Default,,0000,0000,0000,,interval. Right? And so, it didn't do that\Ncorrectly. And the reason for that, maybe
Dialogue: 0,0:33:43.71,0:33:55.01,Default,,0000,0000,0000,,you saw it. So, and, what happened is that\Nit ran into one of those two cases here
Dialogue: 0,0:33:55.01,0:33:59.63,Default,,0000,0000,0000,,where it says if lo1 greater than hi2 or\Nlo2 greater than hi1. Remember that I told
Dialogue: 0,0:33:59.63,0:34:04.63,Default,,0000,0000,0000,,you there needs to be a gap of at least\None between them. Remember? And here's an
Dialogue: 0,0:34:04.63,0:34:11.03,Default,,0000,0000,0000,,off-by-one error that says, well. So this\Nsays, they can, lo1 greater than hi2 says
Dialogue: 0,0:34:11.03,0:34:14.61,Default,,0000,0000,0000,,they can still be right next to each\Nother. Right? And this is what happened
Dialogue: 0,0:34:14.61,0:34:19.76,Default,,0000,0000,0000,,here. We need to make sure that there is\Nthat gap in here. So, I can fix it like
Dialogue: 0,0:34:19.76,0:34:38.06,Default,,0000,0000,0000,,this. Loaded again. Oh, no. There's still\Na counterexample. So, and we can try that
Dialogue: 0,0:34:38.06,0:34:42.94,Default,,0000,0000,0000,,out, so, and that's great. We get test\Ncases that sort of show where the bugs
Dialogue: 0,0:34:42.94,0:34:51.47,Default,,0000,0000,0000,,are. And in this case, well, what happened\Nhere? They still overlap. And what
Dialogue: 0,0:34:51.47,0:34:59.71,Default,,0000,0000,0000,,happened here? So can you see it? So, you\Ncan see that the first two intervals, they
Dialogue: 0,0:34:59.71,0:35:05.44,Default,,0000,0000,0000,,must run into that last case. Right.\NBecause they overlap. Zero is the interval
Dialogue: 0,0:35:05.44,0:35:12.92,Default,,0000,0000,0000,,from 0 to 3 and the interval from 0 to 5.\NThey overlap. So we need to get to that
Dialogue: 0,0:35:12.92,0:35:18.85,Default,,0000,0000,0000,,case. And so it merges them. And then it\Nwent and and somehow didn't merge it with
Dialogue: 0,0:35:18.85,0:35:30.40,Default,,0000,0000,0000,,the 6 and the 7 that's there. And, so,\Nwell, if you look at it. So it must have
Dialogue: 0,0:35:30.40,0:35:38.80,Default,,0000,0000,0000,,done this. And and what it did is, it then\Nwent on with the rest there. Let's have
Dialogue: 0,0:35:38.80,0:35:58.82,Default,,0000,0000,0000,,one more look. What actually happened? So\Nthere it is. So, it merged those and then
Dialogue: 0,0:35:58.82,0:36:02.64,Default,,0000,0000,0000,,you can see that it went into a symmetry\Nproblem here. Well, maybe you don't see.
Dialogue: 0,0:36:02.64,0:36:08.19,Default,,0000,0000,0000,,But, you know, this is tricky stuff. I\Ncouldn't do this by myself. So you can see
Dialogue: 0,0:36:08.19,0:36:18.78,Default,,0000,0000,0000,,here that it just tacks the result onto\Niset1Rest, whereas the maximum of hi1 and
Dialogue: 0,0:36:18.78,0:36:25.89,Default,,0000,0000,0000,,hi2 could, might violate the consistency\Ncriteria if it's the wrong one, and then
Dialogue: 0,0:36:25.89,0:36:30.27,Default,,0000,0000,0000,,it runs into one of the other cases. Now\NI've never seen this tricky one. Does it
Dialogue: 0,0:36:30.27,0:36:34.11,Default,,0000,0000,0000,,make sense? But, can you see that it\Nshould be symmetrical? The last one. Can
Dialogue: 0,0:36:34.11,0:36:39.96,Default,,0000,0000,0000,,you see it? OK, so we'll try and make it\Nsymmetrical. Do it like this. So we'll
Dialogue: 0,0:36:39.96,0:36:51.64,Default,,0000,0000,0000,,say, well, if so, this only works. So if\Nhi1 is less than hi2. So we really need to
Dialogue: 0,0:36:51.64,0:36:59.48,Default,,0000,0000,0000,,make sure, then it is perfectly. And then\Nthe maximum of those two numbers is hi1.
Dialogue: 0,0:36:59.48,0:37:05.38,Default,,0000,0000,0000,,Does that make sense? And so the max of\Nthose two numbers is hi1 and then it's
Dialogue: 0,0:37:05.38,0:37:12.10,Default,,0000,0000,0000,,perfectly valid to tack it onto iset1Rest.\NIn the other case, hi2 is greater and we
Dialogue: 0,0:37:12.10,0:37:18.48,Default,,0000,0000,0000,,need to go and do something different and\Nrip this out here. Stick it in front here
Dialogue: 0,0:37:18.48,0:37:35.95,Default,,0000,0000,0000,,and then. And then. And now it's\Nsymmetrical. OK. So, load this. And, ahh!
Dialogue: 0,0:37:35.95,0:37:40.62,Default,,0000,0000,0000,,It has passed the test. OK, live great.\N{\i1}applause{\i0}
Dialogue: 0,0:37:40.62,0:37:47.10,Default,,0000,0000,0000,,Thank you. I did practice getting it\Ncorrect, right. But you can, you know,
Dialogue: 0,0:37:47.10,0:37:51.34,Default,,0000,0000,0000,,this kind of stuff. It always gets me. I\Nmean, you know, with old age especially,
Dialogue: 0,0:37:51.34,0:37:55.53,Default,,0000,0000,0000,,this kind of stuff, it always drives the\Nsweat on my forehead, right? You know,
Dialogue: 0,0:37:55.53,0:37:59.34,Default,,0000,0000,0000,,there's off-by-one. There is, you know, I\Ndon't know how many cases there need to
Dialogue: 0,0:37:59.34,0:38:03.14,Default,,0000,0000,0000,,be. And QuickCheck is the kind of thing\Nthat weeds out the bugs. And even though
Dialogue: 0,0:38:03.14,0:38:07.06,Default,,0000,0000,0000,,it weeds out the bugs in a different order\Neach time, it always weeds them all out.
Dialogue: 0,0:38:07.06,0:38:11.77,Default,,0000,0000,0000,,OK. So it's a great tool. Now, I recommend\Nthat you try that. It generates tests from
Dialogue: 0,0:38:11.77,0:38:18.87,Default,,0000,0000,0000,,properties. OK, where are we? So let me\Nlet me give you a couple of real world
Dialogue: 0,0:38:18.87,0:38:23.03,Default,,0000,0000,0000,,examples. So if you're using X windows,\Nthere's a there's a tiling, a window
Dialogue: 0,0:38:23.03,0:38:26.89,Default,,0000,0000,0000,,manager, xmonad. It's already a couple of\Nyears old and they don't do much
Dialogue: 0,0:38:26.89,0:38:33.33,Default,,0000,0000,0000,,development on it anymore. That's because\Nit's correct. Right. {\i1}laughter{\i0} Right. And
Dialogue: 0,0:38:33.33,0:38:39.28,Default,,0000,0000,0000,,why is it correct? Well, it's because they\Nwrote down a lot of properties for the
Dialogue: 0,0:38:39.28,0:38:45.69,Default,,0000,0000,0000,,geometry and the tiling algorithms and\Nverified them using QuickCheck. And so I
Dialogue: 0,0:38:45.69,0:38:49.12,Default,,0000,0000,0000,,sort of loosely translated. So, Don\NStewart, one of the authors of xmonad
Dialogue: 0,0:38:49.12,0:38:53.34,Default,,0000,0000,0000,,graciously wrote a couple of blog posts on\Na simplified version of xmonad and I
Dialogue: 0,0:38:53.34,0:39:01.58,Default,,0000,0000,0000,,translated them into Idris. So, here's a\Nvery simple idea of just a stacking window
Dialogue: 0,0:39:01.58,0:39:05.28,Default,,0000,0000,0000,,manager. So, it doesn't do geometry, it\Njust has stacks of windows and it has
Dialogue: 0,0:39:05.28,0:39:10.46,Default,,0000,0000,0000,,several workspaces. In each workspace is a\Nstack of windows. So here's a data type
Dialogue: 0,0:39:10.46,0:39:17.03,Default,,0000,0000,0000,,called a StackSet, its parameterized by a\Ntype called window. We'll see later why
Dialogue: 0,0:39:17.03,0:39:20.93,Default,,0000,0000,0000,,there's a type parameter and why it just\Ndoesn't say what the windows are. And then
Dialogue: 0,0:39:20.93,0:39:25.14,Default,,0000,0000,0000,,it says there's a constructor StackSet\Nand there's two fields in there. One is
Dialogue: 0,0:39:25.14,0:39:34.07,Default,,0000,0000,0000,,called "current", that's the number of the\Nworkspace that's currently
Dialogue: 0,0:39:34.07,0:39:37.46,Default,,0000,0000,0000,,active. And then there's "stacks",\Nwhich is a map from the number of the
Dialogue: 0,0:39:37.46,0:39:44.07,Default,,0000,0000,0000,,workspace to the stack of, to the list of\Nwindows that sit in that workspace. Again,
Dialogue: 0,0:39:44.07,0:39:48.27,Default,,0000,0000,0000,,so here, really the technicalities are\Nnot particularly important, but there is a
Dialogue: 0,0:39:48.27,0:39:54.09,Default,,0000,0000,0000,,bunch of operations that operate on this\Nwindow manager configuration. And again,
Dialogue: 0,0:39:54.09,0:39:58.30,Default,,0000,0000,0000,,here, really the details aren't important.\NSo you could create an empty stack set.
Dialogue: 0,0:39:58.30,0:40:03.35,Default,,0000,0000,0000,,You could say, well, you know, I have the\Nnumber of a window that I want to get to
Dialogue: 0,0:40:03.35,0:40:07.27,Default,,0000,0000,0000,,the front. And please make me, please\Nrotate me, the stack set around so that I
Dialogue: 0,0:40:07.27,0:40:12.99,Default,,0000,0000,0000,,can see it. "peek" means, you know, maybe\NI can get the topmost window that the user
Dialogue: 0,0:40:12.99,0:40:17.07,Default,,0000,0000,0000,,is currently looking at. "rotate" means\NI'm just going to rotate the workspaces
Dialogue: 0,0:40:17.07,0:40:21.03,Default,,0000,0000,0000,,around in either left or right direction.\NThat's what that ordering argument. "push"
Dialogue: 0,0:40:21.03,0:40:25.66,Default,,0000,0000,0000,,is, I push a new window onto the current\Nworkspace. "insert" means insert a window
Dialogue: 0,0:40:25.66,0:40:31.63,Default,,0000,0000,0000,,into one of the other workspaces. "delete"\Nmeans I delete a window. "shift" means,
Dialogue: 0,0:40:31.63,0:40:35.72,Default,,0000,0000,0000,,also means I shift something with the\Nwindows. Not really important what they
Dialogue: 0,0:40:35.72,0:40:42.52,Default,,0000,0000,0000,,do. But you can imagine again, just as we\Ndid with the interval sets is validity
Dialogue: 0,0:40:42.52,0:40:46.82,Default,,0000,0000,0000,,criterion or an invariant that should hold\Nfor these operations. And it's very
Dialogue: 0,0:40:46.82,0:40:51.39,Default,,0000,0000,0000,,simple. Well, it says well, if you have a\Nstack set with some windows in it, I'm
Dialogue: 0,0:40:51.39,0:40:55.32,Default,,0000,0000,0000,,just going to tell you whether that stack\Nset is consistent. And by doing that, I'm
Dialogue: 0,0:40:55.32,0:41:01.80,Default,,0000,0000,0000,,just going to say, well, the current, the\Nnumber of the current stack
Dialogue: 0,0:41:01.80,0:41:07.28,Default,,0000,0000,0000,,should not be higher than the number of\Nwindow stacks that there are. Right. So,
Dialogue: 0,0:41:07.28,0:41:11.05,Default,,0000,0000,0000,,the number of stacks that there are. And\Nthe other one, that just says a window
Dialogue: 0,0:41:11.05,0:41:18.28,Default,,0000,0000,0000,,should not be in several of the\Nworkspaces. Right? And then I can go and
Dialogue: 0,0:41:18.28,0:41:22.91,Default,,0000,0000,0000,,maybe with this definition, all\Nthose function definitions aren't very
Dialogue: 0,0:41:22.91,0:41:26.95,Default,,0000,0000,0000,,complicated. But, I can go and write a\Nwhole bunch of properties. And if you just
Dialogue: 0,0:41:26.95,0:41:30.80,Default,,0000,0000,0000,,understand, well, maybe the second one,\N"prop_view_I", you understand all of them.
Dialogue: 0,0:41:30.80,0:41:35.77,Default,,0000,0000,0000,,It just says, well, for all pairs of a\Nnatural number and a stack set that are a
Dialogue: 0,0:41:35.77,0:41:39.97,Default,,0000,0000,0000,,"stackIndex" and "stackSet", I want, if I\Ncall the "view" function, which is one of
Dialogue: 0,0:41:39.97,0:41:45.02,Default,,0000,0000,0000,,the operations, I want the view function\Nto produce a consistent stack set. And
Dialogue: 0,0:41:45.02,0:41:50.22,Default,,0000,0000,0000,,then it goes on to do all of that for all\Nthe other ones. At the bottom here, you
Dialogue: 0,0:41:50.22,0:41:53.93,Default,,0000,0000,0000,,can see some prerequisites that need to\Nhold for the property so that invariant
Dialogue: 0,0:41:53.93,0:41:59.36,Default,,0000,0000,0000,,only needs to hold if the window, if the\Nnumber of the window is actually smaller
Dialogue: 0,0:41:59.36,0:42:05.12,Default,,0000,0000,0000,,than the size of the stack set. Otherwise,\NI think the function just returns what
Dialogue: 0,0:42:05.12,0:42:09.85,Default,,0000,0000,0000,,would go with it, what went in there, So\Nthat's a very, that's just a very
Dialogue: 0,0:42:09.85,0:42:13.90,Default,,0000,0000,0000,,efficient way to invent properties, to\Nthink of some invariant that shall hold in
Dialogue: 0,0:42:13.90,0:42:17.49,Default,,0000,0000,0000,,your data structure. And if you know\NIdris, you can sometimes encode that in
Dialogue: 0,0:42:17.49,0:42:21.15,Default,,0000,0000,0000,,the types, but often that's kind of\Ntedious. And you can just write it down as
Dialogue: 0,0:42:21.15,0:42:25.75,Default,,0000,0000,0000,,a property and then have QuickCheck check\Nit for you. And it's not particularly
Dialogue: 0,0:42:25.75,0:42:29.79,Default,,0000,0000,0000,,exciting for the simple definition, but\Nyou can imagine that the actual definition
Dialogue: 0,0:42:29.79,0:42:33.71,Default,,0000,0000,0000,,when you have tiling window management\Ngoing on is much more complicated than the
Dialogue: 0,0:42:33.71,0:42:38.42,Default,,0000,0000,0000,,one that you just saw. But you can keep\Nthose same properties, right? There still
Dialogue: 0,0:42:38.42,0:42:42.17,Default,,0000,0000,0000,,needs to be some consistency invariant\Nthat, if you have tilings, the windows
Dialogue: 0,0:42:42.17,0:42:46.15,Default,,0000,0000,0000,,don't overlap, and things like that. That\Nshould be obvious. Write those properties
Dialogue: 0,0:42:46.15,0:42:51.45,Default,,0000,0000,0000,,down, check them using QuickCheck and that\Nwill weed out a lot of the bugs.
Dialogue: 0,0:42:51.45,0:42:55.90,Default,,0000,0000,0000,,Here's an example from our\Npractice. We, couple months ago, we were
Dialogue: 0,0:42:55.90,0:43:03.22,Default,,0000,0000,0000,,tasked with migrating a giant Visual Basic\N6 application. It had a password checking
Dialogue: 0,0:43:03.22,0:43:07.12,Default,,0000,0000,0000,,function there. You can see here a Visual\NBasic 6 type signature. And the property
Dialogue: 0,0:43:07.12,0:43:14.69,Default,,0000,0000,0000,,that we wrote was, well, if we create the\Nhash from the password and we compare it
Dialogue: 0,0:43:14.69,0:43:19.59,Default,,0000,0000,0000,,with the hash that's in the database, then\Nthey should all come out the same. And to
Dialogue: 0,0:43:19.59,0:43:23.61,Default,,0000,0000,0000,,our surprise, that function, that test,\Nthat property, failed when we ran it for
Dialogue: 0,0:43:23.61,0:43:29.41,Default,,0000,0000,0000,,QuickCheck and we had to correct it\Nbecause that password hash is restricted
Dialogue: 0,0:43:29.41,0:43:36.60,Default,,0000,0000,0000,,to 11 characters by some restriction in\Nthe database schema. And so that means
Dialogue: 0,0:43:36.60,0:43:40.33,Default,,0000,0000,0000,,that you can use QuickCheck not just to\Nsort of check the correctness of things
Dialogue: 0,0:43:40.33,0:43:44.49,Default,,0000,0000,0000,,that you already know, but to actually\Ndevelop a model for what goes on in your
Dialogue: 0,0:43:44.49,0:43:50.78,Default,,0000,0000,0000,,software, which you don't always know very\Nwell. So that's what we did there. Another
Dialogue: 0,0:43:50.78,0:43:57.09,Default,,0000,0000,0000,,example is, we wrote, for a large\Nindustrial client, we needed to write a
Dialogue: 0,0:43:57.09,0:44:01.20,Default,,0000,0000,0000,,synchronization application. So when you\Nhad two mobile devices and they would sort
Dialogue: 0,0:44:01.20,0:44:05.77,Default,,0000,0000,0000,,of meet as strangers, they would exchange\Ndata and they all needed to look at the
Dialogue: 0,0:44:05.77,0:44:10.94,Default,,0000,0000,0000,,same sort of device configuration data.\NAnd we didn't want them to exchange all
Dialogue: 0,0:44:10.94,0:44:15.23,Default,,0000,0000,0000,,the data every single time. We just wanted\Nto exchange them, the data blocks that the
Dialogue: 0,0:44:15.23,0:44:20.84,Default,,0000,0000,0000,,other side was missing. And again, there's\Ngreat algorithms for this based on Merkle
Dialogue: 0,0:44:20.84,0:44:24.47,Default,,0000,0000,0000,,trees. They're pretty complicated. You\Nhave to do a lot of bit fiddling with
Dialogue: 0,0:44:24.47,0:44:28.95,Default,,0000,0000,0000,,that. But fortunately, the property for\Nthat is pretty easy to write. So here's
Dialogue: 0,0:44:28.95,0:44:34.43,Default,,0000,0000,0000,,the property that says, well, so the\Nsynchronization algorithm works on sets of
Dialogue: 0,0:44:34.43,0:44:39.91,Default,,0000,0000,0000,,blocks, whatever a block is. So you can\Nsee the property here for all pairs of
Dialogue: 0,0:44:39.91,0:44:45.13,Default,,0000,0000,0000,,sets of blocks and more sets of blocks. So\Nthey're called bs1 and bs2. Block set one
Dialogue: 0,0:44:45.13,0:44:53.03,Default,,0000,0000,0000,,and block set two. What we can do is, we\Nwant, if we union those two, then we get
Dialogue: 0,0:44:53.03,0:44:57.27,Default,,0000,0000,0000,,all the blocks in the system. We call that\Nall, or we can call the synchronization
Dialogue: 0,0:44:57.27,0:45:05.49,Default,,0000,0000,0000,,algorithm and that will give us two new\Nblock sets, block set bs1' and bs2'. And
Dialogue: 0,0:45:05.49,0:45:10.94,Default,,0000,0000,0000,,those block sets are the ones that get\Ntransferred to the other side. OK. And the
Dialogue: 0,0:45:10.94,0:45:16.15,Default,,0000,0000,0000,,criterion here just says if we take the\Nones that we have, if we union them with
Dialogue: 0,0:45:16.15,0:45:20.19,Default,,0000,0000,0000,,the ones that we get, we should get all of\Nthem. That should be all of them. And that
Dialogue: 0,0:45:20.19,0:45:24.53,Default,,0000,0000,0000,,should be the same for both sides. And\Nalso, we want the algorithm to be
Dialogue: 0,0:45:24.53,0:45:28.85,Default,,0000,0000,0000,,efficient so we don't want it to transfer\Nblocks. So we want to make sure that the
Dialogue: 0,0:45:28.85,0:45:32.88,Default,,0000,0000,0000,,blocks that we have and the blocks that we\Nget are disjoint. That they don't have any
Dialogue: 0,0:45:32.88,0:45:37.77,Default,,0000,0000,0000,,elements in common. Otherwise, we could\Nmake that algorithm trivially correct by
Dialogue: 0,0:45:37.77,0:45:42.42,Default,,0000,0000,0000,,just transferring all the blocks every\Nsingle time. And I can tell you, I
Dialogue: 0,0:45:42.42,0:45:46.06,Default,,0000,0000,0000,,sweated. You know, I sweated one or two\Nweeks over this algorithm and it was
Dialogue: 0,0:45:46.06,0:45:52.79,Default,,0000,0000,0000,,really hard to write. But this one test\Nweeded out all the bugs that I found along
Dialogue: 0,0:45:52.79,0:45:58.73,Default,,0000,0000,0000,,the way. So that is just super, super\Neffective. John Hughes has a couple of
Dialogue: 0,0:45:58.73,0:46:02.86,Default,,0000,0000,0000,,papers on hard bugs that he found. So he\Nfound a bug in a distributed database
Dialogue: 0,0:46:02.86,0:46:09.60,Default,,0000,0000,0000,,called mnesia. And that bug was dependent\Non opening the database, closing it and
Dialogue: 0,0:46:09.60,0:46:14.65,Default,,0000,0000,0000,,opening it again. So this is not the kind\Nof bug that you find by just writing a
Dialogue: 0,0:46:14.65,0:46:19.71,Default,,0000,0000,0000,,bunch of smart unit tests. Right? So, if\Nyou did anything shorter in the beginning,
Dialogue: 0,0:46:19.71,0:46:24.98,Default,,0000,0000,0000,,so if you just open the file and then did\Nsome lookups there, that would not
Dialogue: 0,0:46:24.98,0:46:29.32,Default,,0000,0000,0000,,manifest the bug. You really needed to\Nclose and then open again. Have you
Dialogue: 0,0:46:29.32,0:46:33.83,Default,,0000,0000,0000,,turned, have you tried turning it off and\Non again? But then the database breaks in
Dialogue: 0,0:46:33.83,0:46:39.00,Default,,0000,0000,0000,,this case. And here's another example\Ncalled The Mysteries of Dropbox. So you
Dialogue: 0,0:46:39.00,0:46:45.94,Default,,0000,0000,0000,,can imagine that with Dropbox you really\Nwant certain properties to hold. Right?
Dialogue: 0,0:46:45.94,0:46:50.03,Default,,0000,0000,0000,,And it turns out they didn't. They never\Nworried about writing properties down. But
Dialogue: 0,0:46:50.03,0:46:54.70,Default,,0000,0000,0000,,John Hughes did it and found a couple of\Nbugs. So here's one. It's kind of hard to
Dialogue: 0,0:46:54.70,0:47:00.71,Default,,0000,0000,0000,,read where it says client 1 writes a into\Na file that was previously empty. So that
Dialogue: 0,0:47:00.71,0:47:07.17,Default,,0000,0000,0000,,funky turnstile there is empty. So writes\Na into a file and then deletes the file
Dialogue: 0,0:47:07.17,0:47:12.22,Default,,0000,0000,0000,,and another client writes, replaces, sees\Nthe a in the file replaces it with a b.
Dialogue: 0,0:47:12.22,0:47:18.34,Default,,0000,0000,0000,,And then client 1 goes and writes c into\Nthe file that it previously thought to be
Dialogue: 0,0:47:18.34,0:47:23.19,Default,,0000,0000,0000,,empty. And then unfortunately, even though\Nyou can imagine that you should see either
Dialogue: 0,0:47:23.19,0:47:28.66,Default,,0000,0000,0000,,b or c in that file, but Dropbox deleted\Nit. So I think they fixed that bug now.
Dialogue: 0,0:47:28.66,0:47:37.13,Default,,0000,0000,0000,,But. so you go. So it goes. Oscar Wikstrom\Nhas a couple of great, pretty recent blog
Dialogue: 0,0:47:37.13,0:47:44.74,Default,,0000,0000,0000,,posts on properties in a screencasts\Neditor that I highly recommend. So this is
Dialogue: 0,0:47:44.74,0:47:51.20,Default,,0000,0000,0000,,a great tool for finding bugs, but it's\Nnot the same as having a proof. Right? So,
Dialogue: 0,0:47:51.20,0:47:56.15,Default,,0000,0000,0000,,you can still imagine that you can find\Nvery subtle bugs that are not covered by
Dialogue: 0,0:47:56.15,0:48:00.04,Default,,0000,0000,0000,,QuickCheck. QuickCheck just randomizes,\Njust generates randomized tests. So, that
Dialogue: 0,0:48:00.04,0:48:06.51,Default,,0000,0000,0000,,is not the same thing as making sure that\Nthere aren't any bugs. So the great thing
Dialogue: 0,0:48:06.51,0:48:10.96,Default,,0000,0000,0000,,about Idris and the reason I chose it for\Nthis talk is that Idris allows you to not
Dialogue: 0,0:48:10.96,0:48:15.53,Default,,0000,0000,0000,,just encode properties in the language. It\Nalso allows you to encode proofs in the
Dialogue: 0,0:48:15.53,0:48:20.72,Default,,0000,0000,0000,,language. So here is the associative\Nproperty for the list concatenation
Dialogue: 0,0:48:20.72,0:48:24.64,Default,,0000,0000,0000,,operation. And if you look at the top that\Nhas the definition of that function from
Dialogue: 0,0:48:24.64,0:48:30.10,Default,,0000,0000,0000,,the Idris standard library, it says ++, in\Ngoes a list, in goes another list, out
Dialogue: 0,0:48:30.10,0:48:35.73,Default,,0000,0000,0000,,comes a list. Then it says, well, if you\Nconcatenate the empty list with any list,
Dialogue: 0,0:48:35.73,0:48:41.08,Default,,0000,0000,0000,,that is just that list "right". Do you\Nsee that? The second one says, well, if we
Dialogue: 0,0:48:41.08,0:48:45.51,Default,,0000,0000,0000,,concatenate a list that starts with the\Nelement x and goes on with xs, then we
Dialogue: 0,0:48:45.51,0:48:50.83,Default,,0000,0000,0000,,just sort of pull the x in front and\Nconcatenate the rest with "right". So
Dialogue: 0,0:48:50.83,0:48:54.89,Default,,0000,0000,0000,,that's a classic recursive definition of\Nlist concatenation in functional
Dialogue: 0,0:48:54.89,0:48:59.06,Default,,0000,0000,0000,,programming. And now here's something\Nreally strange in Idris. Here's the type
Dialogue: 0,0:48:59.06,0:49:04.01,Default,,0000,0000,0000,,declaration for a definition, again in the\Nstandard library, called appendAssoc. And
Dialogue: 0,0:49:04.01,0:49:09.18,Default,,0000,0000,0000,,it says, if you have a list a, you have a\Nlist b, and you have a list c, and in the
Dialogue: 0,0:49:09.18,0:49:14.96,Default,,0000,0000,0000,,type it says, oh, the associative property\Nshould hold. Right. And so this is a
Dialogue: 0,0:49:14.96,0:49:20.98,Default,,0000,0000,0000,,statement of that property. That's\Nwonderful. It's not the same as a proof.
Dialogue: 0,0:49:20.98,0:49:29.69,Default,,0000,0000,0000,,So, but writing proofs, who loved that in\Nmath? Oh. Oh, you're good! I didn't. I'm
Dialogue: 0,0:49:29.69,0:49:33.90,Default,,0000,0000,0000,,sorry. So. So the great thing about Idris\Nis, it helps you write down the proofs.
Dialogue: 0,0:49:33.90,0:49:38.73,Default,,0000,0000,0000,,I'll show you how that works just really,\Nreally briefly. So here's that. So here's
Dialogue: 0,0:49:38.73,0:49:42.69,Default,,0000,0000,0000,,just what I showed you on that slide. So I\Ncan load that in there and it says, well,
Dialogue: 0,0:49:42.69,0:49:46.56,Default,,0000,0000,0000,,you're not done. You didn't write a proof\Nfor that property, but in Idris, you can
Dialogue: 0,0:49:46.56,0:49:50.90,Default,,0000,0000,0000,,just push a bunch of buttons. Now, I love\Nthat. So I can push one button and it
Dialogue: 0,0:49:50.90,0:49:55.36,Default,,0000,0000,0000,,says, oh, well, you should write a proof\Nof that form. You have lists a, b and c.
Dialogue: 0,0:49:55.36,0:49:59.38,Default,,0000,0000,0000,,Well, now and I can push another button\Nthat says, well, you're doing this on
Dialogue: 0,0:49:59.38,0:50:04.80,Default,,0000,0000,0000,,lists and if you're writing anything on\Nlists, you always need to distinguish
Dialogue: 0,0:50:04.80,0:50:09.00,Default,,0000,0000,0000,,between the two cases of the empty list\Nand the list that consists of the first
Dialogue: 0,0:50:09.00,0:50:14.59,Default,,0000,0000,0000,,element x and further element xs. And then\Nit says, well, write down something, but
Dialogue: 0,0:50:14.59,0:50:18.71,Default,,0000,0000,0000,,then I can tell Idris: Well, I'm too lazy.\NI'm not going to write anything so I can
Dialogue: 0,0:50:18.71,0:50:23.06,Default,,0000,0000,0000,,just push a button. And Idris wrote this\Nso you can see me, but I didn't type this
Dialogue: 0,0:50:23.06,0:50:29.36,Default,,0000,0000,0000,,right. I just pushed a button and it says,\NRefl. What is Refl? What could that be?
Dialogue: 0,0:50:29.36,0:50:35.81,Default,,0000,0000,0000,,Well, you can ask it what Refl is. It says\NRefl. Oh, you can see here, landing here.
Dialogue: 0,0:50:35.81,0:50:39.53,Default,,0000,0000,0000,,Refl is just a proof sort of a built in\Nproof that says that if two things are
Dialogue: 0,0:50:39.53,0:50:44.72,Default,,0000,0000,0000,,true, two things are equal, if they're\Nidentical, if they're the same. Right. And
Dialogue: 0,0:50:44.72,0:50:48.59,Default,,0000,0000,0000,,that kind of makes sense in the first\Nequation, because the first equation of
Dialogue: 0,0:50:48.59,0:50:53.42,Default,,0000,0000,0000,,appendAssoc corresponds to the first\Nequation of ++. Can you see that, how it
Dialogue: 0,0:50:53.42,0:51:01.42,Default,,0000,0000,0000,,corresponds? Can you see that? The first\Nlist is empty. Can you see that? Can you
Dialogue: 0,0:51:01.42,0:51:05.18,Default,,0000,0000,0000,,see how the first list is empty with the\Nfirst equation of appendAssoc and the
Dialogue: 0,0:51:05.18,0:51:13.70,Default,,0000,0000,0000,,first list is empty up there with ++. Can\Nyou see that? OK. And then it just says,
Dialogue: 0,0:51:13.70,0:51:18.50,Default,,0000,0000,0000,,well, then obviously. Well, not quite\Nobviously, but then sort of the the way
Dialogue: 0,0:51:18.50,0:51:22.65,Default,,0000,0000,0000,,that the definition works, it comes out\Njust right. So what's really important is
Dialogue: 0,0:51:22.65,0:51:27.74,Default,,0000,0000,0000,,that Idris accepts that proof with the\Nfirst. The second one is slightly more
Dialogue: 0,0:51:27.74,0:51:35.96,Default,,0000,0000,0000,,tricky. But again, we can get help because\Nwe know that appendAssoc is this recursive
Dialogue: 0,0:51:35.96,0:51:39.48,Default,,0000,0000,0000,,function. It recurses on the first\Nargument. So we're just going to do the
Dialogue: 0,0:51:39.48,0:51:47.28,Default,,0000,0000,0000,,same thing in the proof. And you can tell\NIdris that it should use that, that it
Dialogue: 0,0:51:47.28,0:51:52.44,Default,,0000,0000,0000,,should use that fact, if you will. So\Nhere's the recursive call. And again, I'm
Dialogue: 0,0:51:52.44,0:51:56.44,Default,,0000,0000,0000,,too lazy to push a button. But if I push\Nthat button, it also puts in Refl and
Dialogue: 0,0:51:56.44,0:52:02.26,Default,,0000,0000,0000,,there's loads. So this it might be a\Nmystery to you how it works, but this is a
Dialogue: 0,0:52:02.26,0:52:06.98,Default,,0000,0000,0000,,proof of the associate of property of the\Nlist concatenation in Idris. And since
Dialogue: 0,0:52:06.98,0:52:12.19,Default,,0000,0000,0000,,Idris helps you write it, it's kind of fun\Nto do that. Oddly enough, even for
Dialogue: 0,0:52:12.19,0:52:16.09,Default,,0000,0000,0000,,somebody who doesn't, usually who doesn't\Nusually doesn't enjoy proofs. So the way
Dialogue: 0,0:52:16.09,0:52:22.07,Default,,0000,0000,0000,,that you program in Idris, we haven't done\Nthat a lot in this talk, is that you put a
Dialogue: 0,0:52:22.07,0:52:26.28,Default,,0000,0000,0000,,lot of information in the types and the\Nmore information you put in the types, the
Dialogue: 0,0:52:26.28,0:52:30.32,Default,,0000,0000,0000,,better Idris will get at figuring out the\Ncorrect definition. And you don't have to
Dialogue: 0,0:52:30.32,0:52:38.89,Default,,0000,0000,0000,,do it by yourself. OK. So that's really\Nnice. OK. So we got that and and sort of
Dialogue: 0,0:52:38.89,0:52:43.79,Default,,0000,0000,0000,,these kinds of proof assisting systems\Nsuch as Idris have been used in a lot of
Dialogue: 0,0:52:43.79,0:52:48.99,Default,,0000,0000,0000,,real world systems. One one prominent\Nexample is SEL4, a version of the L4
Dialogue: 0,0:52:48.99,0:52:52.81,Default,,0000,0000,0000,,micro kernel, has a long history, but\Nimportant properties of that kernel have
Dialogue: 0,0:52:52.81,0:52:57.41,Default,,0000,0000,0000,,been verified. It runs in the security\Nenclave on iOS and even though it's
Dialogue: 0,0:52:57.41,0:53:01.28,Default,,0000,0000,0000,,written in C, it provably does not have\Nbuffer overflows or a lot of the nasty
Dialogue: 0,0:53:01.28,0:53:06.16,Default,,0000,0000,0000,,things that are responsible for a lot of\Nsecurity exploits. Compcert is another
Dialogue: 0,0:53:06.16,0:53:11.31,Default,,0000,0000,0000,,example, which is a verified, I should\Nmention this has been verified with the
Dialogue: 0,0:53:11.31,0:53:15.69,Default,,0000,0000,0000,,help of a tool called Isabel. Also, great\Nfun to use. There's a project called
Dialogue: 0,0:53:15.69,0:53:20.39,Default,,0000,0000,0000,,called Compcert, which is a verified C\Ncompiler, which is important for a lot of
Dialogue: 0,0:53:20.39,0:53:24.36,Default,,0000,0000,0000,,certified software where, you know, the\Nsource code might be certified. But how do
Dialogue: 0,0:53:24.36,0:53:29.61,Default,,0000,0000,0000,,you know that the compiler generates\Ncorrect code? And you know, because it's
Dialogue: 0,0:53:29.61,0:53:34.43,Default,,0000,0000,0000,,been proven to be correct. And even there,\Nyou can shoot, you can cheat sometimes. So
Dialogue: 0,0:53:34.43,0:53:38.05,Default,,0000,0000,0000,,for example, register allocators, very\Ncomplicated, very hard to prove right.
Dialogue: 0,0:53:38.05,0:53:41.71,Default,,0000,0000,0000,,But what you can do is you can write a\Nchecker that the register allocator did
Dialogue: 0,0:53:41.71,0:53:47.81,Default,,0000,0000,0000,,its job, did its job well and you can\Nverify the checker. And so you can cheat a
Dialogue: 0,0:53:47.81,0:53:52.15,Default,,0000,0000,0000,,bit. So there's tools for that. We've seen\NIdris and there's a number of other tools
Dialogue: 0,0:53:52.15,0:53:56.51,Default,,0000,0000,0000,,and they're getting more and more mature.\NAnd they're great fun, really. They really
Dialogue: 0,0:53:56.51,0:54:01.54,Default,,0000,0000,0000,,are great fun. But, you know, going back,\Nswitching down a gear a little bit,
Dialogue: 0,0:54:01.54,0:54:05.13,Default,,0000,0000,0000,,there's lots of useful properties that you\Ncan look for in your programs. So
Dialogue: 0,0:54:05.13,0:54:09.97,Default,,0000,0000,0000,,commutativity might be useful that you can\Nswitch the two arguments for an operation.
Dialogue: 0,0:54:09.97,0:54:13.79,Default,,0000,0000,0000,,Also, if you have relations, you might\Nremember that from some math class,
Dialogue: 0,0:54:13.79,0:54:17.58,Default,,0000,0000,0000,,there's some properties here like\Nreflexivity, symmetry, antisymmetry and
Dialogue: 0,0:54:17.58,0:54:24.32,Default,,0000,0000,0000,,transitivity. Reflexivity says that a is\Nalways related to a. Symmetry says if it's
Dialogue: 0,0:54:24.32,0:54:28.92,Default,,0000,0000,0000,,one way, if a and b are one way related,\Nthey need to be related the other way too.
Dialogue: 0,0:54:28.92,0:54:32.84,Default,,0000,0000,0000,,Antisymmetry intuitively would seem kind\Nof the opposite. That doesn't make sense.
Dialogue: 0,0:54:32.84,0:54:38.77,Default,,0000,0000,0000,,It's just says: if two things are related\Nin both both ways around. So, for example,
Dialogue: 0,0:54:38.77,0:54:43.37,Default,,0000,0000,0000,,you know, orders like less or equal are\Nantisymmetrical, then they must be the
Dialogue: 0,0:54:43.37,0:54:47.82,Default,,0000,0000,0000,,same. And transitivity just says that you\Ncan form chains of your relation. So those
Dialogue: 0,0:54:47.82,0:54:53.26,Default,,0000,0000,0000,,are a little dictionary of useful\Nproperties that you can look for. Let me
Dialogue: 0,0:54:53.26,0:54:58.30,Default,,0000,0000,0000,,close with one fancy property that you've\Nprobably seen somewhere and that property
Dialogue: 0,0:54:58.30,0:55:03.81,Default,,0000,0000,0000,,is called Functor. And you might have seen\Nin your programing language, in your list
Dialogue: 0,0:55:03.81,0:55:08.54,Default,,0000,0000,0000,,library or in your stream library. There's\Na function called map, right? And you
Dialogue: 0,0:55:08.54,0:55:13.91,Default,,0000,0000,0000,,know, even Java has that and has had it\Nfor many years. And what map does is, if
Dialogue: 0,0:55:13.91,0:55:18.67,Default,,0000,0000,0000,,you have some, you know, in Java, for\Nexample, it says "Stream", or it might be
Dialogue: 0,0:55:18.67,0:55:22.64,Default,,0000,0000,0000,,"List", right. It says, well, if I have a\Nlist of As, I can apply a function to each
Dialogue: 0,0:55:22.64,0:55:26.98,Default,,0000,0000,0000,,element of that list. But you can\Ngeneralize that, it doesn't have to be
Dialogue: 0,0:55:26.98,0:55:31.19,Default,,0000,0000,0000,,lists. It could be an Optional of As, for\Nexample. You could also apply a function
Dialogue: 0,0:55:31.19,0:55:35.32,Default,,0000,0000,0000,,to the value that's in there. So, you can\Ngeneralize that notion, and then it's a
Dialogue: 0,0:55:35.32,0:55:42.69,Default,,0000,0000,0000,,functor. And, of course, in Idris, you can\Nwrite down equations for functors. And,
Dialogue: 0,0:55:42.69,0:55:47.66,Default,,0000,0000,0000,,please ignore the technicalities here,\N(stammers) but, if you sort of pick out
Dialogue: 0,0:55:47.66,0:55:52.20,Default,,0000,0000,0000,,where it says "functorIdentity",\Nthe middle row says g v equals to v,
Dialogue: 0,0:55:52.20,0:55:56.00,Default,,0000,0000,0000,,which means g is the identity\Nfunction. When you feed in v, you always
Dialogue: 0,0:55:56.00,0:56:00.64,Default,,0000,0000,0000,,get v back. And when you use map with the\Nidentity function, you apply the identity
Dialogue: 0,0:56:00.64,0:56:05.53,Default,,0000,0000,0000,,function on each element of your list or\Nwhatever it is. Then then you always get
Dialogue: 0,0:56:05.53,0:56:10.99,Default,,0000,0000,0000,,back the same list. And here just says you\Nget function composition. So if you apply
Dialogue: 0,0:56:10.99,0:56:14.93,Default,,0000,0000,0000,,one function and then another function and\Nyou do that either inside or outside the
Dialogue: 0,0:56:14.93,0:56:18.49,Default,,0000,0000,0000,,map, you should also get the same results.\NSo there's also just as there is
Dialogue: 0,0:56:18.49,0:56:24.23,Default,,0000,0000,0000,,associativity with monoids, with functors.\NThere's these laws and you might think,
Dialogue: 0,0:56:24.23,0:56:27.100,Default,,0000,0000,0000,,well, where would I look for a functor?\NI've never seen a functor except for the
Dialogue: 0,0:56:27.100,0:56:31.96,Default,,0000,0000,0000,,ones on streams. A couple weeks ago in a\Ntraining, somebody said, well, you always
Dialogue: 0,0:56:31.96,0:56:38.79,Default,,0000,0000,0000,,start with that animal example. Shouldn't\Nyou look for a functor there? And I was
Dialogue: 0,0:56:38.79,0:56:42.84,Default,,0000,0000,0000,,kind of, you know, sweat broke out on my\Nforehead, I was like, where's that gonna
Dialogue: 0,0:56:42.84,0:56:47.33,Default,,0000,0000,0000,,go? But, we came up with this. So, if you\Ngo back, you can see that this is obvious.
Dialogue: 0,0:56:47.33,0:56:52.22,Default,,0000,0000,0000,,So, what you need for functors is, you\Nneed a type parameter. Right. And so you
Dialogue: 0,0:56:52.22,0:56:55.74,Default,,0000,0000,0000,,just look for a place to stick a type\Nparameter, any place here at all. And
Dialogue: 0,0:56:55.74,0:56:59.44,Default,,0000,0000,0000,,if you look at Dillo and Parrot, they\Nboth prominently have this weight thing.
Dialogue: 0,0:56:59.44,0:57:03.20,Default,,0000,0000,0000,,Right. And so that seems more important\Nthan the other two properties, which are
Dialogue: 0,0:57:03.20,0:57:09.59,Default,,0000,0000,0000,,specific to particular kind of animal. And\Nso the weight, the thing to do is just to,
Dialogue: 0,0:57:09.59,0:57:14.06,Default,,0000,0000,0000,,well, you can see I replaced upper case\NWeight by lower case weight and made that
Dialogue: 0,0:57:14.06,0:57:19.81,Default,,0000,0000,0000,,into a type parameter, and, I can then\Nprovide a functor implementation down
Dialogue: 0,0:57:19.81,0:57:23.58,Default,,0000,0000,0000,,there. And you might think, what is that\Ngood for? Well, I don't know. Well, one
Dialogue: 0,0:57:23.58,0:57:27.11,Default,,0000,0000,0000,,thing that you could do is you could\Nprovide a different representation for
Dialogue: 0,0:57:27.11,0:57:31.07,Default,,0000,0000,0000,,weights. Another thing that you could do,\Nif you look at the type for runOverAnimal,
Dialogue: 0,0:57:31.07,0:57:35.82,Default,,0000,0000,0000,,it says animal weight -> animal weight and\Nweight is a type variable. What that type
Dialogue: 0,0:57:35.82,0:57:41.12,Default,,0000,0000,0000,,signature tells you is that runOverAnimal\Ndoes not know what weight is. And that
Dialogue: 0,0:57:41.12,0:57:45.63,Default,,0000,0000,0000,,means that the weight cannot change as a\Nresult of that function. And you see that
Dialogue: 0,0:57:45.63,0:57:49.65,Default,,0000,0000,0000,,in the type signature you get immediate,\Nsmall benefit, but you get a benefit even
Dialogue: 0,0:57:49.65,0:57:55.59,Default,,0000,0000,0000,,with silly examples such as this one. And\Nthat really brings me to the end. So in
Dialogue: 0,0:57:55.59,0:58:00.48,Default,,0000,0000,0000,,your software, in your domain model, look\Nfor a Combinator, look for a function that
Dialogue: 0,0:58:00.48,0:58:05.80,Default,,0000,0000,0000,,will combine two things into a bigger\Nthing. See if you can make that thing
Dialogue: 0,0:58:05.80,0:58:09.61,Default,,0000,0000,0000,,associative and look for a neutral\Nelement. And very often you will find one;
Dialogue: 0,0:58:09.61,0:58:13.49,Default,,0000,0000,0000,,make it a monoid, you know, say monoid a\Ncouple of times. You'll remember it.
Dialogue: 0,0:58:13.49,0:58:17.46,Default,,0000,0000,0000,,You'll remember it. Generally, write\Nproperties for the things, for the
Dialogue: 0,0:58:17.46,0:58:23.39,Default,,0000,0000,0000,,operations in your software, test those\Nproperties using QuickCheck. You know, if
Dialogue: 0,0:58:23.39,0:58:27.77,Default,,0000,0000,0000,,you feel like you have a lot of time,\Nprove them correct. Find the functor. If
Dialogue: 0,0:58:27.77,0:58:32.39,Default,,0000,0000,0000,,you found, if you found the monoid, you\Nknow, find the functor next. You know, and
Dialogue: 0,0:58:32.39,0:58:35.96,Default,,0000,0000,0000,,it takes, it might take time. I'm\Nvery old. As you noticed at the beginning.
Dialogue: 0,0:58:35.96,0:58:42.19,Default,,0000,0000,0000,,So. So it gets easier over the years and\Nit will just seem like a regular staple of
Dialogue: 0,0:58:42.19,0:58:47.10,Default,,0000,0000,0000,,your of your arsenal when you program. And\Nof course, when the important properties
Dialogue: 0,0:58:47.10,0:58:51.07,Default,,0000,0000,0000,,in your program have either been written\Ndown, if they've been tested with
Dialogue: 0,0:58:51.07,0:58:54.84,Default,,0000,0000,0000,,QuickCheck or even proven, then you can\Nsleep much more soundly than maybe you
Dialogue: 0,0:58:54.84,0:59:04.82,Default,,0000,0000,0000,,currently can. Thank you very much.\N{\i1}applause{\i0}
Dialogue: 0,0:59:04.82,0:59:10.84,Default,,0000,0000,0000,,Herald: Thank you, Mike. So I see we have\Nthree minutes for questions. Maybe that's
Dialogue: 0,0:59:10.84,0:59:16.12,Default,,0000,0000,0000,,two or three questions. If you have any\Ncome to the microphones, please. Do we
Dialogue: 0,0:59:16.12,0:59:25.95,Default,,0000,0000,0000,,have a question from the Internet? No, not\Nyet. So, microphone two. Right.
Dialogue: 0,0:59:25.95,0:59:34.05,Default,,0000,0000,0000,,Question: Hi. So, QuickCheck generated\Nhundred tests. Yes. What can we say about
Dialogue: 0,0:59:34.05,0:59:38.58,Default,,0000,0000,0000,,the quality of this test? Could we say\Nyour program was correct using thoese
Dialogue: 0,0:59:38.58,0:59:42.56,Default,,0000,0000,0000,,tests? Are these tests good?\NAnswer: Yeah. Very good question. So what
Dialogue: 0,0:59:42.56,0:59:46.38,Default,,0000,0000,0000,,would you say about the quality of the\Ntests? And indeed, if you really do serve
Dialogue: 0,0:59:46.38,0:59:50.76,Default,,0000,0000,0000,,industrial strength applications, a quick\NQuickCheck comes with a bunch of tools
Dialogue: 0,0:59:50.76,0:59:54.88,Default,,0000,0000,0000,,that let you look, for example, at the\Ndistribution of the individual example
Dialogue: 0,0:59:54.88,1:00:02.25,Default,,0000,0000,0000,,rated and while you didn't quite see me do\Nthat, but I mean, for your domain objects,
Dialogue: 0,1:00:02.25,1:00:06.15,Default,,0000,0000,0000,,you will typically write generators that\Nwill generate those examples and you can
Dialogue: 0,1:00:06.15,1:00:09.99,Default,,0000,0000,0000,,reason about the distribution of those.\NAnd you absolutely should do that because
Dialogue: 0,1:00:09.99,1:00:15.42,Default,,0000,0000,0000,,otherwise you might miss large areas of\Nyour test space. So, but there
Dialogue: 0,1:00:15.42,1:00:20.39,Default,,0000,0000,0000,,are tools and they help you do that. But\Neven if you don't do that, you know, it's,
Dialogue: 0,1:00:20.39,1:00:24.26,Default,,0000,0000,0000,,you find a lot of, I found a lot of\Nbugs in my software even without worrying
Dialogue: 0,1:00:24.26,1:00:28.56,Default,,0000,0000,0000,,about that. But if you go beyond that,\Nlook at the distribution thing.
Dialogue: 0,1:00:28.56,1:00:34.36,Default,,0000,0000,0000,,Herald: Thank you, next one, please.\NNumber two.
Dialogue: 0,1:00:34.36,1:00:40.66,Default,,0000,0000,0000,,Q: Let's say I've hacked a program, for\Nexample, in Java or C# or whatever. How do
Dialogue: 0,1:00:40.66,1:00:50.08,Default,,0000,0000,0000,,I, how do I apply what I learned so\Nfar? So, where do I start when I have
Dialogue: 0,1:00:50.08,1:00:57.69,Default,,0000,0000,0000,,already completed the C# program with,\Nyeah, how do I apply QuickCheck on that?
Dialogue: 0,1:00:57.69,1:01:01.23,Default,,0000,0000,0000,,A: So, just pragmatically because it's\Nwritten in C#? That's the question?
Dialogue: 0,1:01:01.23,1:01:03.72,Default,,0000,0000,0000,,Q: Yes\NA: So, well, I have to be very concrete
Dialogue: 0,1:01:03.72,1:01:07.84,Default,,0000,0000,0000,,here, I mean, so, if you can think\Nproperties, right, one way to do, so,
Dialogue: 0,1:01:07.84,1:01:14.79,Default,,0000,0000,0000,,for example, so, C# you can link with F#\Nand there is a QuickCheck version for F#
Dialogue: 0,1:01:14.79,1:01:19.09,Default,,0000,0000,0000,,called "FsCheck". And FsCheck, actually,\Neven though it's itself written in F#, you
Dialogue: 0,1:01:19.09,1:01:23.46,Default,,0000,0000,0000,,can also use it from C#. So, you have two\Noptions. You can write your tests in a
Dialogue: 0,1:01:23.46,1:01:28.49,Default,,0000,0000,0000,,slightly more awkward fashion in C#, or\Nyou could just link your code with F# test
Dialogue: 0,1:01:28.49,1:01:35.33,Default,,0000,0000,0000,,suite and write it down there. And there\Nis a fairly reasonable Java QuickCheck, I
Dialogue: 0,1:01:35.33,1:01:39.53,Default,,0000,0000,0000,,hear. Another idea would be to use the\Nslightly more fancier, the slightly
Dialogue: 0,1:01:39.53,1:01:45.15,Default,,0000,0000,0000,,fancier QuickChecks that exist for Scala\Nand Enclosure. I'm sure there's one for
Dialogue: 0,1:01:45.15,1:01:49.22,Default,,0000,0000,0000,,Kotlin as well, and link that against your\NJava code. Does that answer your question?
Dialogue: 0,1:01:49.22,1:01:54.51,Default,,0000,0000,0000,,Q: So whatever language I use, I have to\Nfind out what the correct implementation
Dialogue: 0,1:01:54.51,1:01:56.89,Default,,0000,0000,0000,,of QuickCkeck?\NA: Yeah. Yeah. But as I said, I mean
Dialogue: 0,1:01:56.89,1:02:00.80,Default,,0000,0000,0000,,usually, a fun thing I do in training is,\NI chat "QuickCheck" and somebody calls on
Dialogue: 0,1:02:00.80,1:02:04.68,Default,,0000,0000,0000,,the language, you know. Quick, QuickCheck\NPHP or something like that. And there is
Dialogue: 0,1:02:04.68,1:02:07.99,Default,,0000,0000,0000,,one, sure enough, I didn't know about before.\NQ: Thank you.
Dialogue: 0,1:02:07.99,1:02:12.14,Default,,0000,0000,0000,,Herald: All right. Thank you. And thank\Nyou, Mike, again, for showing us a way to
Dialogue: 0,1:02:12.14,1:02:15.25,Default,,0000,0000,0000,,sleeping soundly.\NA: Thank you.
Dialogue: 0,1:02:15.25,1:02:20.65,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,1:02:20.65,1:02:27.11,Default,,0000,0000,0000,,{\i1}postroll music{\i0}
Dialogue: 0,1:02:27.11,1:02:45.60,Default,,0000,0000,0000,,Subtitles created by c3subtitles.de\Nin the year 2020. Join, and help us!