0 00:00:00,000 --> 00:00:30,000 Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/384 Thanks! 1 00:00:09,570 --> 00:00:10,919 So thanks. 2 00:00:10,920 --> 00:00:11,939 Yeah, my name is Rachel. 3 00:00:11,940 --> 00:00:13,469 I'm one of the people who occasionally 4 00:00:13,470 --> 00:00:14,570 hack on the compiler. 5 00:00:15,600 --> 00:00:16,829 Yeah. And today I'm going to talk a 6 00:00:16,830 --> 00:00:18,389 little bit about programing with the 7 00:00:18,390 --> 00:00:20,069 types and address. 8 00:00:20,070 --> 00:00:22,529 So this talk is for people who 9 00:00:22,530 --> 00:00:23,559 don't really know what the dependent 10 00:00:23,560 --> 00:00:25,859 types are and are curious about it. 11 00:00:25,860 --> 00:00:28,139 If you know what cockies or ACDA, then 12 00:00:28,140 --> 00:00:30,239 you will be probably bored. 13 00:00:30,240 --> 00:00:32,309 So yeah, I can't help, but maybe 14 00:00:32,310 --> 00:00:33,509 there is something new for you, who 15 00:00:33,510 --> 00:00:34,510 knows. 16 00:00:35,010 --> 00:00:36,929 So I will be talking about obviously 17 00:00:36,930 --> 00:00:38,999 dependent types and a thing that's called 18 00:00:39,000 --> 00:00:40,709 the Curry Howard correspondance. 19 00:00:40,710 --> 00:00:42,469 One question is this large enough? 20 00:00:42,470 --> 00:00:44,340 You know, OK, let's make the bigger 21 00:00:46,170 --> 00:00:47,159 better. 22 00:00:47,160 --> 00:00:48,539 OK, so 23 00:00:49,980 --> 00:00:51,399 I think that's called the Currey our 24 00:00:51,400 --> 00:00:53,159 correspondence, which is in my opinion, a 25 00:00:53,160 --> 00:00:55,439 very powerful mental model to reason 26 00:00:55,440 --> 00:00:57,779 about types as propositions. 27 00:00:57,780 --> 00:00:59,339 So we'll introduce that and we'll talk a 28 00:00:59,340 --> 00:01:00,780 little bit about constructive logic 29 00:01:01,860 --> 00:01:04,079 and how we can model this 30 00:01:04,080 --> 00:01:06,119 in the type system so we can have more 31 00:01:06,120 --> 00:01:07,439 expressive types. 32 00:01:07,440 --> 00:01:10,049 I'll do a little bit of life coding and 33 00:01:10,050 --> 00:01:12,209 hopefully everything will work out right. 34 00:01:12,210 --> 00:01:14,249 I don't know. Sometimes things fail, so 35 00:01:14,250 --> 00:01:15,250 please don't laugh at me. 36 00:01:16,500 --> 00:01:18,089 And in the end I will talk about effects 37 00:01:18,090 --> 00:01:20,249 and typewriters. So it was just a purely 38 00:01:20,250 --> 00:01:21,389 functional programing language. 39 00:01:21,390 --> 00:01:23,579 Therefore, we have to have some 40 00:01:23,580 --> 00:01:25,349 mechanism to deal with side effects, 41 00:01:25,350 --> 00:01:27,569 stuff like IO, writing 42 00:01:27,570 --> 00:01:29,309 to files, communicating with the outside 43 00:01:29,310 --> 00:01:31,409 world, stuff like that. 44 00:01:31,410 --> 00:01:33,899 And we reflect that and the type system. 45 00:01:33,900 --> 00:01:35,999 And another thing is that 46 00:01:36,000 --> 00:01:38,129 which is a pretty nice thing 47 00:01:38,130 --> 00:01:39,119 is typewriters. 48 00:01:39,120 --> 00:01:41,309 So we can do side effects on 49 00:01:41,310 --> 00:01:41,999 the type level. 50 00:01:42,000 --> 00:01:43,769 That might sound a little bit weird if 51 00:01:43,770 --> 00:01:45,389 you are. 52 00:01:45,390 --> 00:01:47,669 Yeah. Work with language like C++ 53 00:01:47,670 --> 00:01:49,949 or other ones. 54 00:01:49,950 --> 00:01:52,409 Why should we have type system 55 00:01:52,410 --> 00:01:53,669 effects on the type level? 56 00:01:53,670 --> 00:01:55,679 But I hope I can convince you that this 57 00:01:55,680 --> 00:01:56,760 is a pretty nice thing to have. 58 00:01:58,260 --> 00:02:00,029 So what is it? Reciters is a purely 59 00:02:00,030 --> 00:02:01,349 functional programing language that is 60 00:02:01,350 --> 00:02:02,519 developed by Aaron Brady. 61 00:02:02,520 --> 00:02:04,619 It's developed on GitHub and 62 00:02:04,620 --> 00:02:06,089 so you can download the code, go crazy 63 00:02:06,090 --> 00:02:07,469 with it. Simple request. 64 00:02:07,470 --> 00:02:09,779 That's what I did. A lot of fun and 65 00:02:09,780 --> 00:02:11,279 it's currently intended as a research 66 00:02:11,280 --> 00:02:13,049 tool. So please don't use this in 67 00:02:13,050 --> 00:02:15,149 production. I've seen people who 68 00:02:15,150 --> 00:02:16,829 wanted to do that. I wanted to do that 69 00:02:16,830 --> 00:02:18,869 too. But you will figure out pretty 70 00:02:18,870 --> 00:02:20,100 quickly that you shouldn't do it. 71 00:02:21,780 --> 00:02:23,309 Say it's a purely functional programing 72 00:02:23,310 --> 00:02:24,809 language. If you're familiar with Haskell 73 00:02:24,810 --> 00:02:26,969 or similar languages, it will 74 00:02:26,970 --> 00:02:29,249 feel pretty much at home to you. 75 00:02:29,250 --> 00:02:30,479 Of course, it's your to type. 76 00:02:30,480 --> 00:02:32,159 This is this is why we're interested in 77 00:02:32,160 --> 00:02:34,229 it. And the syntax is pretty close 78 00:02:34,230 --> 00:02:36,359 to Haskell. So some minor 79 00:02:36,360 --> 00:02:38,489 differences here. And there are, 80 00:02:38,490 --> 00:02:40,679 of course, different semantics, but we're 81 00:02:40,680 --> 00:02:41,909 not going to talk about that too much 82 00:02:41,910 --> 00:02:44,129 here. And what I find 83 00:02:44,130 --> 00:02:45,779 particularly appealing about the language 84 00:02:45,780 --> 00:02:47,909 is that it's it focuses on 85 00:02:47,910 --> 00:02:49,379 general purpose programing. 86 00:02:49,380 --> 00:02:52,199 So if you've got a system like Sakurada, 87 00:02:52,200 --> 00:02:54,299 it's more like a proof existence. 88 00:02:54,300 --> 00:02:56,309 So you want to prove mathematical 89 00:02:56,310 --> 00:02:58,739 theorems or theorems of actual software 90 00:02:58,740 --> 00:03:00,929 and character, but you don't really 91 00:03:00,930 --> 00:03:03,239 want to write a web server or 92 00:03:03,240 --> 00:03:05,039 similar stuff and that that gets a little 93 00:03:05,040 --> 00:03:06,040 bit hairy. 94 00:03:07,440 --> 00:03:09,569 So this is actually one of 95 00:03:09,570 --> 00:03:11,159 the major selling points of interest. 96 00:03:11,160 --> 00:03:13,199 In fact these slides are written in 97 00:03:13,200 --> 00:03:16,319 address, that computer JavaScript. 98 00:03:16,320 --> 00:03:17,549 That's the project I've been working on 99 00:03:17,550 --> 00:03:18,839 for a couple of years now. 100 00:03:18,840 --> 00:03:20,909 So you can try it out and 101 00:03:20,910 --> 00:03:23,099 write some JavaScript Web 102 00:03:23,100 --> 00:03:24,419 applications or notes. 103 00:03:24,420 --> 00:03:25,349 If you don't want to write pure 104 00:03:25,350 --> 00:03:26,459 JavaScript, which is. 105 00:03:26,460 --> 00:03:27,720 Yeah, don't want to. 106 00:03:28,980 --> 00:03:30,599 So another thing that's pretty 107 00:03:30,600 --> 00:03:32,609 interesting is its totality checking so 108 00:03:32,610 --> 00:03:35,009 we can check if 109 00:03:35,010 --> 00:03:37,799 an algorithm actually terminates. 110 00:03:37,800 --> 00:03:39,659 Ah, that might sound a little weird as 111 00:03:39,660 --> 00:03:41,879 well because halting problem. 112 00:03:41,880 --> 00:03:43,829 But if we don't have things like general 113 00:03:43,830 --> 00:03:46,019 recursion and just reduce 114 00:03:46,020 --> 00:03:48,659 ourselves to use print of recursion, 115 00:03:48,660 --> 00:03:50,219 then we can actually prove that an 116 00:03:50,220 --> 00:03:51,220 algorithm terminates. 117 00:03:52,950 --> 00:03:55,379 We also have interactive proving with 118 00:03:55,380 --> 00:03:56,849 tactics. I'm not going to talk about 119 00:03:56,850 --> 00:03:58,139 that, but it's there. 120 00:03:58,140 --> 00:04:00,059 Obviously, we have a lot less tactics 121 00:04:00,060 --> 00:04:02,129 than COK, which has an insane 122 00:04:02,130 --> 00:04:03,809 amount of tactics. 123 00:04:03,810 --> 00:04:04,709 So what's the motivation? 124 00:04:04,710 --> 00:04:07,019 Why do we want more expressive 125 00:04:07,020 --> 00:04:08,759 type systems? Because there are a lot of 126 00:04:08,760 --> 00:04:10,319 very exciting type systems out there. 127 00:04:11,400 --> 00:04:13,649 So I get to make the smaller but 128 00:04:13,650 --> 00:04:16,289 only for this slight excuse me. 129 00:04:16,290 --> 00:04:18,749 Cell types are 130 00:04:18,750 --> 00:04:21,208 a very, very effective way to keep 131 00:04:21,209 --> 00:04:23,519 our program behavior in check 132 00:04:23,520 --> 00:04:26,099 so we can guarantee 133 00:04:26,100 --> 00:04:28,709 that some things don't happen at runtime 134 00:04:28,710 --> 00:04:31,229 when our type system is, well, checking 135 00:04:31,230 --> 00:04:33,269 all these things so you can have a 136 00:04:33,270 --> 00:04:35,339 function that you can guarantee 137 00:04:35,340 --> 00:04:37,379 that this function only gets an integer 138 00:04:37,380 --> 00:04:38,380 and not a string. 139 00:04:39,240 --> 00:04:41,339 That's pretty much 140 00:04:41,340 --> 00:04:43,199 the least thing a type system can do for 141 00:04:43,200 --> 00:04:45,839 you, but it's something so 142 00:04:45,840 --> 00:04:47,579 when you have a very powerful programing 143 00:04:47,580 --> 00:04:47,819 language. 144 00:04:47,820 --> 00:04:49,919 So this is not a risk. This is C++, 145 00:04:49,920 --> 00:04:51,989 which has a very, very powerful type 146 00:04:51,990 --> 00:04:53,129 system. 147 00:04:53,130 --> 00:04:54,909 The template system by itself is too 148 00:04:54,910 --> 00:04:56,549 incomplete. It's completely insane. 149 00:04:57,660 --> 00:04:59,849 And so in this example, I'm 150 00:04:59,850 --> 00:05:01,949 I'm just trying to model a 151 00:05:01,950 --> 00:05:04,049 conditional branch, something if then 152 00:05:04,050 --> 00:05:06,119 else on the type level might seem 153 00:05:06,120 --> 00:05:07,949 a little bit contrived, but we'll get to 154 00:05:07,950 --> 00:05:09,249 an example where this is. 155 00:05:09,250 --> 00:05:10,250 A useful thing to do, 156 00:05:11,370 --> 00:05:13,769 so you and see 157 00:05:13,770 --> 00:05:15,509 if then else is a pretty simple thing, 158 00:05:15,510 --> 00:05:17,729 but just to have it on the type level, 159 00:05:17,730 --> 00:05:20,039 we got to write this weird code 160 00:05:20,040 --> 00:05:21,119 over there. 161 00:05:21,120 --> 00:05:22,679 And that leads to a very interesting 162 00:05:22,680 --> 00:05:25,439 observation that when you are programing 163 00:05:25,440 --> 00:05:27,629 in a static type programing language, 164 00:05:27,630 --> 00:05:29,729 you're usually working in two different 165 00:05:29,730 --> 00:05:30,689 languages. 166 00:05:30,690 --> 00:05:32,669 So you're working and the value language 167 00:05:32,670 --> 00:05:34,739 that you programed most of the 168 00:05:34,740 --> 00:05:36,799 time. And so you write all your programs 169 00:05:36,800 --> 00:05:38,939 on the value level and you've got the 170 00:05:38,940 --> 00:05:41,369 type level language that is used 171 00:05:41,370 --> 00:05:43,169 to program on your type level. 172 00:05:43,170 --> 00:05:44,249 And that's a completely different 173 00:05:44,250 --> 00:05:45,839 language. You have to learn two 174 00:05:45,840 --> 00:05:47,309 languages. You get two for the price of 175 00:05:47,310 --> 00:05:49,649 one, which is not very good because 176 00:05:49,650 --> 00:05:51,809 you have to duplicate a lot of stuff 177 00:05:51,810 --> 00:05:53,909 that you want to reuse on the type level 178 00:05:53,910 --> 00:05:55,379 like this branch. 179 00:05:56,550 --> 00:05:58,109 So we want to unify that. 180 00:05:58,110 --> 00:05:59,969 We just want to work with terms. 181 00:05:59,970 --> 00:06:01,559 And that is something where dependent 182 00:06:01,560 --> 00:06:04,349 types are quite handy, especially IDers. 183 00:06:04,350 --> 00:06:06,179 So what are dependent types? 184 00:06:06,180 --> 00:06:08,009 This is a little bit of a watered down 185 00:06:08,010 --> 00:06:10,019 view of what types are. 186 00:06:10,020 --> 00:06:12,719 This is not like the full blown whatever 187 00:06:12,720 --> 00:06:15,189 lambda cube, yada yada yada stuff. 188 00:06:15,190 --> 00:06:17,459 So this is just very, very simple. 189 00:06:17,460 --> 00:06:19,349 If you want to know the whole story, read 190 00:06:19,350 --> 00:06:21,749 up on the Lamba Cube on stuff like sorts 191 00:06:21,750 --> 00:06:22,769 and kinds. 192 00:06:22,770 --> 00:06:25,499 But I just want to give you a basic 193 00:06:25,500 --> 00:06:26,730 idea of what this is. 194 00:06:27,780 --> 00:06:29,069 And first of all, we got to talk about 195 00:06:29,070 --> 00:06:31,050 what a dependency is so 196 00:06:32,520 --> 00:06:35,129 we can have values that depend on values. 197 00:06:35,130 --> 00:06:36,759 That's a pretty simple thing. 198 00:06:36,760 --> 00:06:37,799 We do that all the time. That's a 199 00:06:37,800 --> 00:06:38,699 function. 200 00:06:38,700 --> 00:06:40,229 So we can write a function. 201 00:06:40,230 --> 00:06:42,329 We could put a value into that and 202 00:06:42,330 --> 00:06:44,309 we had a result. And that result depends 203 00:06:44,310 --> 00:06:45,989 on the value that we feed into the 204 00:06:45,990 --> 00:06:47,099 function. 205 00:06:47,100 --> 00:06:49,229 That's a very simple function over there. 206 00:06:49,230 --> 00:06:50,589 That's the increment function is just 207 00:06:50,590 --> 00:06:52,469 takes a natural number and gives us a 208 00:06:52,470 --> 00:06:53,549 natural number. It gives us the 209 00:06:53,550 --> 00:06:54,550 successor. 210 00:06:55,650 --> 00:06:56,870 You can see that the 211 00:06:58,200 --> 00:06:59,670 up there this is 212 00:07:01,320 --> 00:07:02,369 excuse me. 213 00:07:02,370 --> 00:07:04,589 So this is the type signature 214 00:07:04,590 --> 00:07:06,479 to make this a little bit larger. 215 00:07:06,480 --> 00:07:08,249 So that's better. 216 00:07:08,250 --> 00:07:10,079 And this is the implementation. 217 00:07:10,080 --> 00:07:11,969 So it just takes an argument X 218 00:07:11,970 --> 00:07:13,379 incremented by one. 219 00:07:13,380 --> 00:07:15,660 So very simple function on. 220 00:07:16,800 --> 00:07:18,449 Another thing that might be interesting 221 00:07:18,450 --> 00:07:19,559 to you, if you don't know programing 222 00:07:19,560 --> 00:07:21,029 languages like Haskell, we do functional 223 00:07:21,030 --> 00:07:23,069 applications just by saying nothing. 224 00:07:23,070 --> 00:07:24,269 So no parentheses. 225 00:07:24,270 --> 00:07:25,799 This is function application. 226 00:07:25,800 --> 00:07:28,439 So normally you write F parents, 227 00:07:28,440 --> 00:07:31,019 whatever, and we don't do it that way. 228 00:07:31,020 --> 00:07:33,029 So that's some sort of dependency that we 229 00:07:33,030 --> 00:07:34,979 want to have. We want to have values that 230 00:07:34,980 --> 00:07:35,980 values, obviously. 231 00:07:37,050 --> 00:07:38,789 So another thing that might be 232 00:07:38,790 --> 00:07:41,339 interesting is we want to take type's 233 00:07:41,340 --> 00:07:42,599 to values. 234 00:07:42,600 --> 00:07:44,729 So think about the 235 00:07:44,730 --> 00:07:46,169 identity function, the identity 236 00:07:46,170 --> 00:07:47,639 functions. It just does nothing. 237 00:07:47,640 --> 00:07:49,499 It just takes a value and returns the 238 00:07:49,500 --> 00:07:50,500 value unmodified. 239 00:07:51,540 --> 00:07:53,489 So when you have a lot of types, you have 240 00:07:53,490 --> 00:07:54,929 to come up with a lot of different 241 00:07:54,930 --> 00:07:56,189 implementation of the idea of the 242 00:07:56,190 --> 00:07:57,389 identity function, which is pretty 243 00:07:57,390 --> 00:07:58,559 boring. 244 00:07:58,560 --> 00:08:00,809 So you want to write one identity 245 00:08:00,810 --> 00:08:02,790 function that binds them all. 246 00:08:03,840 --> 00:08:05,939 So you want to have a type as 247 00:08:05,940 --> 00:08:07,799 an argument and then it returns a 248 00:08:07,800 --> 00:08:09,899 function that can deal with 249 00:08:09,900 --> 00:08:11,009 these things. 250 00:08:11,010 --> 00:08:13,109 So in this case, we just 251 00:08:13,110 --> 00:08:15,419 take a type A as an argument and 252 00:08:15,420 --> 00:08:17,549 we return a function which is a value 253 00:08:17,550 --> 00:08:18,570 from AA. 254 00:08:19,950 --> 00:08:22,019 So here we 255 00:08:22,020 --> 00:08:23,559 are using that. 256 00:08:23,560 --> 00:08:25,689 So it takes that and that is the 257 00:08:25,690 --> 00:08:27,189 type of natural numbers, which is just 258 00:08:27,190 --> 00:08:29,529 zero, one, two, three, yada, yada, 259 00:08:29,530 --> 00:08:31,929 and we turn it on modified. 260 00:08:31,930 --> 00:08:33,459 So what's interesting about this is that 261 00:08:33,460 --> 00:08:35,589 you can see we do type application 262 00:08:35,590 --> 00:08:38,269 just the same way as we're doing it 263 00:08:38,270 --> 00:08:40,058 with values. 264 00:08:40,059 --> 00:08:42,399 So there's something weird going on. 265 00:08:42,400 --> 00:08:45,069 If you've got a like C++, 266 00:08:45,070 --> 00:08:46,419 you have these angled brackets or 267 00:08:46,420 --> 00:08:48,549 Scollard, you've got square brackets to 268 00:08:48,550 --> 00:08:49,599 type up a patient here. 269 00:08:49,600 --> 00:08:51,939 This just feels like a value. 270 00:08:51,940 --> 00:08:53,979 This is we're starting to get into the 271 00:08:53,980 --> 00:08:55,809 realm of what it was really about. 272 00:08:57,040 --> 00:08:59,169 So another example is just the same 273 00:08:59,170 --> 00:09:00,170 thing with strings. 274 00:09:01,780 --> 00:09:03,459 So another thing, another dependancy. 275 00:09:03,460 --> 00:09:05,529 One half is want to have types 276 00:09:05,530 --> 00:09:06,729 that depend on types. 277 00:09:06,730 --> 00:09:09,009 So think about data structures. 278 00:09:09,010 --> 00:09:11,379 So this is this is a linear list and 279 00:09:11,380 --> 00:09:13,569 we want to build linear lists for every 280 00:09:13,570 --> 00:09:14,709 type. 281 00:09:14,710 --> 00:09:15,710 So 282 00:09:16,930 --> 00:09:17,979 this is a type constructor. 283 00:09:17,980 --> 00:09:19,929 It takes a type and it returns a new 284 00:09:19,930 --> 00:09:21,999 type. So can say list, feed 285 00:09:22,000 --> 00:09:24,729 and string and you get a list of string 286 00:09:24,730 --> 00:09:26,859 and this this type 287 00:09:26,860 --> 00:09:28,989 of stuff. Constructors, it has Knill, 288 00:09:28,990 --> 00:09:30,639 which is just the empty list. 289 00:09:30,640 --> 00:09:32,649 And this thing is pronounced KONE's. 290 00:09:32,650 --> 00:09:35,439 We just we can take a value, take a list, 291 00:09:35,440 --> 00:09:37,179 put the value in front of it and we get a 292 00:09:37,180 --> 00:09:39,609 new list. So we're inductively generating 293 00:09:39,610 --> 00:09:40,610 that list. 294 00:09:41,650 --> 00:09:43,779 So here is an example. 295 00:09:43,780 --> 00:09:44,739 We just have the list. 296 00:09:44,740 --> 00:09:46,749 One, two, three, four, and we end with 297 00:09:46,750 --> 00:09:47,769 the empty list. 298 00:09:47,770 --> 00:09:49,749 That's a little bit clunky to write 299 00:09:49,750 --> 00:09:51,249 because we're using the special kind of 300 00:09:51,250 --> 00:09:52,269 syntax over there. 301 00:09:52,270 --> 00:09:54,429 We can use this 302 00:09:54,430 --> 00:09:56,589 very convenient list syntax to to 303 00:09:56,590 --> 00:09:58,779 express that. So this is constructor 304 00:09:58,780 --> 00:10:01,419 overloading. We can do that for 305 00:10:01,420 --> 00:10:02,469 pretty much a lot of things. 306 00:10:03,520 --> 00:10:05,649 So in 307 00:10:05,650 --> 00:10:07,749 case you might notice, this little 308 00:10:07,750 --> 00:10:09,789 single quote, this is just part of the 309 00:10:09,790 --> 00:10:11,949 identifier. This is nothing special. 310 00:10:11,950 --> 00:10:14,229 This is just so that I don't name 311 00:10:14,230 --> 00:10:15,619 clash with the actual list in the 312 00:10:15,620 --> 00:10:16,620 preview. 313 00:10:19,870 --> 00:10:21,879 So, yeah, now we've got three different 314 00:10:21,880 --> 00:10:22,849 kinds of dependencies. 315 00:10:22,850 --> 00:10:24,759 So there's just one thing missing. 316 00:10:24,760 --> 00:10:26,229 And that's the thing that you're missing 317 00:10:26,230 --> 00:10:28,449 in most of the programing languages where 318 00:10:28,450 --> 00:10:30,819 you've got where you can take values 319 00:10:30,820 --> 00:10:31,849 to types. 320 00:10:31,850 --> 00:10:33,609 That's that's the new thing. 321 00:10:33,610 --> 00:10:35,529 This is what what we mean when we talk 322 00:10:35,530 --> 00:10:36,639 about dependent types. 323 00:10:36,640 --> 00:10:39,519 We can have types that depend on values. 324 00:10:39,520 --> 00:10:41,649 So this is a string that 325 00:10:41,650 --> 00:10:44,019 string vector and this vector is just 326 00:10:44,020 --> 00:10:46,059 it's basically a list, but with the 327 00:10:46,060 --> 00:10:48,339 length in the type. 328 00:10:48,340 --> 00:10:50,439 So we we have additional information 329 00:10:50,440 --> 00:10:52,989 in our type that says, OK, this 330 00:10:52,990 --> 00:10:55,569 this vector is of length four 331 00:10:55,570 --> 00:10:56,570 or whatever. 332 00:10:57,190 --> 00:10:59,499 So obviously the vector is 333 00:10:59,500 --> 00:11:01,869 length zero and the 334 00:11:01,870 --> 00:11:03,969 case it takes a string, 335 00:11:03,970 --> 00:11:05,889 a string vector of length then. 336 00:11:05,890 --> 00:11:08,019 And what we get is a string vector 337 00:11:08,020 --> 00:11:09,299 of length, one plus end. 338 00:11:10,360 --> 00:11:11,829 And what's interesting about this, this 339 00:11:11,830 --> 00:11:13,879 plus this is not a special type of a 340 00:11:13,880 --> 00:11:16,029 plus. This is the same plus that we're 341 00:11:16,030 --> 00:11:18,039 using on the value level. 342 00:11:18,040 --> 00:11:19,869 So we've got a lot of for use here. 343 00:11:19,870 --> 00:11:22,059 So whenever we've got a function that 344 00:11:22,060 --> 00:11:23,979 we can use on a value level, we can use 345 00:11:23,980 --> 00:11:26,109 that on the type level as long as it's 346 00:11:26,110 --> 00:11:27,610 total. And yeah. 347 00:11:28,900 --> 00:11:31,119 So this is 348 00:11:31,120 --> 00:11:32,649 just an example. It's the string vector 349 00:11:32,650 --> 00:11:33,579 of like four. 350 00:11:33,580 --> 00:11:34,939 I have four elements. 351 00:11:34,940 --> 00:11:37,329 If I were to delete one of these elements 352 00:11:37,330 --> 00:11:38,799 and obviously it wouldn't compile, would 353 00:11:38,800 --> 00:11:40,359 complain, hey, these lines don't match 354 00:11:40,360 --> 00:11:41,360 up, 355 00:11:42,610 --> 00:11:44,919 OK, this is too large 356 00:11:44,920 --> 00:11:47,019 so we 357 00:11:47,020 --> 00:11:48,189 can have a cake and eat it too. 358 00:11:48,190 --> 00:11:50,439 We can build a vector 359 00:11:50,440 --> 00:11:52,569 that is generic. So this is just the 360 00:11:52,570 --> 00:11:54,279 same thing. String vector isn't very, 361 00:11:54,280 --> 00:11:55,719 very useful because we can only put 362 00:11:55,720 --> 00:11:56,949 strings in there. 363 00:11:56,950 --> 00:11:58,329 So we don't want that. We want a vector 364 00:11:58,330 --> 00:12:00,409 for everything and we also have that 365 00:12:00,410 --> 00:12:01,389 in preload. 366 00:12:01,390 --> 00:12:02,799 So this is a vector. 367 00:12:04,660 --> 00:12:06,699 This is this has got the same 368 00:12:06,700 --> 00:12:08,619 constructors as the list before. 369 00:12:08,620 --> 00:12:10,989 It has the vector with with 370 00:12:10,990 --> 00:12:13,809 length one we also got. 371 00:12:13,810 --> 00:12:15,009 This is the same story. 372 00:12:15,010 --> 00:12:16,839 So now let's implement something that 373 00:12:16,840 --> 00:12:18,819 uses that. And in this case, we want to 374 00:12:18,820 --> 00:12:20,829 implement the append function. 375 00:12:20,830 --> 00:12:23,169 So append takes two vectors, 376 00:12:23,170 --> 00:12:25,059 a vector of length N and the vector of 377 00:12:25,060 --> 00:12:27,219 length M and the result 378 00:12:27,220 --> 00:12:30,039 is a vector of like and plus M, 379 00:12:30,040 --> 00:12:31,839 so the type tells us a lot of what's 380 00:12:31,840 --> 00:12:32,799 going on here. 381 00:12:32,800 --> 00:12:34,459 It's a little bit different, like the 382 00:12:34,460 --> 00:12:36,579 Penford list where we just take a list, a 383 00:12:36,580 --> 00:12:38,559 list, a list, a what does it do. 384 00:12:38,560 --> 00:12:40,659 I don't know, I could just 385 00:12:40,660 --> 00:12:42,100 throw away one of the lists. 386 00:12:44,200 --> 00:12:46,419 So here we are implementing this function 387 00:12:46,420 --> 00:12:48,399 in case the left hand side is the empty 388 00:12:48,400 --> 00:12:49,389 list. 389 00:12:49,390 --> 00:12:51,609 Empty vector. Excuse me, we just return 390 00:12:51,610 --> 00:12:52,610 wise. 391 00:12:53,230 --> 00:12:55,299 If it's the case, 392 00:12:55,300 --> 00:12:57,519 we just take the front element. 393 00:12:57,520 --> 00:12:59,469 We have we put it at the front and we 394 00:12:59,470 --> 00:13:00,519 call upon recursively. 395 00:13:01,750 --> 00:13:02,950 So we just 396 00:13:04,120 --> 00:13:05,619 go through the list, put them together 397 00:13:05,620 --> 00:13:07,359 and voila. 398 00:13:07,360 --> 00:13:09,429 So there are two vectors one would 399 00:13:09,430 --> 00:13:11,919 like for another one with for 400 00:13:11,920 --> 00:13:14,139 we put them together, obviously 401 00:13:14,140 --> 00:13:16,359 higher mathematics, length eight and 402 00:13:16,360 --> 00:13:17,360 that that's great. 403 00:13:18,670 --> 00:13:20,769 So, OK, that's that's 404 00:13:20,770 --> 00:13:21,309 the view. 405 00:13:21,310 --> 00:13:22,310 What. What. 406 00:13:23,040 --> 00:13:25,019 Dependent types are what can do with them 407 00:13:25,020 --> 00:13:26,600 and let's put them to use 408 00:13:27,960 --> 00:13:29,909 and yeah, I want to talk about the 409 00:13:29,910 --> 00:13:31,470 Kurihara correspondence, which, 410 00:13:32,640 --> 00:13:34,199 well, it brings us into the land of 411 00:13:34,200 --> 00:13:35,200 logic. 412 00:13:36,390 --> 00:13:38,399 So there are a lot of logical connectors 413 00:13:38,400 --> 00:13:40,769 out there and or not whatever. 414 00:13:40,770 --> 00:13:42,929 And they actually they have 415 00:13:44,160 --> 00:13:46,229 well, a corresponding type on the 416 00:13:46,230 --> 00:13:47,649 in the Tipler in the title. 417 00:13:47,650 --> 00:13:48,869 And so 418 00:13:50,880 --> 00:13:52,649 when we look at something like this, this 419 00:13:52,650 --> 00:13:53,699 looks very weird. 420 00:13:53,700 --> 00:13:54,809 So this is a type 421 00:13:56,310 --> 00:13:58,589 type with numbers and equals sign. 422 00:13:58,590 --> 00:14:00,539 So we call this this type propositional 423 00:14:00,540 --> 00:14:02,879 equality and 424 00:14:02,880 --> 00:14:05,099 we can only constructed if the two 425 00:14:05,100 --> 00:14:07,199 values on this equal 426 00:14:07,200 --> 00:14:09,299 sign are are the 427 00:14:09,300 --> 00:14:10,300 same thing. 428 00:14:12,390 --> 00:14:14,219 Obviously they are by definition. 429 00:14:14,220 --> 00:14:16,109 Twenty three equals twenty three. 430 00:14:16,110 --> 00:14:17,219 So we can construct it. 431 00:14:17,220 --> 00:14:18,329 This is a common. 432 00:14:18,330 --> 00:14:20,099 This is just the pseudocode that I put up 433 00:14:20,100 --> 00:14:22,289 there. So you can imagine how this looks 434 00:14:22,290 --> 00:14:24,929 like. So it takes two arguments 435 00:14:24,930 --> 00:14:27,449 sometimes something A, B 436 00:14:27,450 --> 00:14:30,389 and we can construct this if 437 00:14:30,390 --> 00:14:31,830 both sides are equal. 438 00:14:34,710 --> 00:14:36,449 And what was interesting about this is 439 00:14:36,450 --> 00:14:38,549 that twenty three equals twenty 440 00:14:38,550 --> 00:14:40,889 three is all is a logical proposition. 441 00:14:40,890 --> 00:14:43,079 So we 442 00:14:43,080 --> 00:14:44,969 say this and we're going to prove that. 443 00:14:44,970 --> 00:14:47,249 And whenever we write a program 444 00:14:47,250 --> 00:14:49,349 that satisfies this type, 445 00:14:49,350 --> 00:14:50,769 we've got a proof. 446 00:14:50,770 --> 00:14:52,889 So proof the program is 447 00:14:52,890 --> 00:14:54,399 a proof. 448 00:14:54,400 --> 00:14:56,099 It's not just a simple program. 449 00:14:56,100 --> 00:14:57,839 We can really use programs as proof. 450 00:14:59,550 --> 00:15:01,799 And this gives us a lot of interesting 451 00:15:01,800 --> 00:15:03,209 possibilities when we want to do 452 00:15:03,210 --> 00:15:05,759 something like test driven development 453 00:15:05,760 --> 00:15:07,379 type driven development where I come 454 00:15:07,380 --> 00:15:09,509 from. So you can't really 455 00:15:09,510 --> 00:15:12,089 write types that 456 00:15:12,090 --> 00:15:13,749 do an exhaustive check. 457 00:15:13,750 --> 00:15:15,869 So you can say for all this 458 00:15:15,870 --> 00:15:18,389 holds, for all values of whatever, 459 00:15:18,390 --> 00:15:20,129 this is a lot better than just a test, 460 00:15:20,130 --> 00:15:21,569 which is pretty much an anecdote. 461 00:15:21,570 --> 00:15:23,609 So I knew I know some values where this 462 00:15:23,610 --> 00:15:25,909 works out and you can do this 463 00:15:25,910 --> 00:15:27,119 in an exhaustive way. 464 00:15:28,560 --> 00:15:29,560 So. 465 00:15:30,320 --> 00:15:32,339 So since we've got logic, we want to have 466 00:15:32,340 --> 00:15:33,570 something like true value. 467 00:15:34,590 --> 00:15:36,509 This is a very trivial case. 468 00:15:36,510 --> 00:15:38,639 So we call the subunit and 469 00:15:38,640 --> 00:15:39,809 has one constructor. 470 00:15:39,810 --> 00:15:41,639 So it's always true. 471 00:15:41,640 --> 00:15:43,859 Whenever I say I want some value 472 00:15:43,860 --> 00:15:46,139 of unit, here is proof. 473 00:15:46,140 --> 00:15:48,179 It's just a simple empty tuple. 474 00:15:49,590 --> 00:15:51,689 We're not using that. But just for the 475 00:15:51,690 --> 00:15:52,690 sake of completeness, 476 00:15:54,270 --> 00:15:56,099 obviously we want to have a notion of 477 00:15:56,100 --> 00:15:57,359 what's false. 478 00:15:57,360 --> 00:15:59,789 So I said that whenever we find a program 479 00:15:59,790 --> 00:16:01,889 that implements type signature, that's 480 00:16:01,890 --> 00:16:02,819 a proof. 481 00:16:02,820 --> 00:16:05,609 So when we don't have a proof, 482 00:16:05,610 --> 00:16:07,709 then this thing has got to be 483 00:16:07,710 --> 00:16:09,359 false. It's an empty type we call an 484 00:16:09,360 --> 00:16:11,279 uninhabited type. 485 00:16:11,280 --> 00:16:13,139 So Voit has no constructors. 486 00:16:13,140 --> 00:16:14,789 We shouldn't be able to construct that. 487 00:16:14,790 --> 00:16:17,149 Sometimes there are bugs in the compiler. 488 00:16:17,150 --> 00:16:19,529 I think recently the COK people 489 00:16:19,530 --> 00:16:21,599 found something where they could 490 00:16:21,600 --> 00:16:23,669 prove false happens all 491 00:16:23,670 --> 00:16:24,839 the time. 492 00:16:24,840 --> 00:16:26,849 It's it's software. 493 00:16:26,850 --> 00:16:29,999 It's still failed, but it's pretty early. 494 00:16:30,000 --> 00:16:31,820 So it's researching. 495 00:16:33,490 --> 00:16:35,160 So, OK, this is the empty type 496 00:16:37,380 --> 00:16:38,819 one. Have another thing which is called 497 00:16:38,820 --> 00:16:40,889 conjunction. So when I want to prove A 498 00:16:40,890 --> 00:16:42,689 and B a true, I want to give a 499 00:16:42,690 --> 00:16:44,939 construction for that. And so once 500 00:16:44,940 --> 00:16:47,039 again, I'm using propositional quality 501 00:16:47,040 --> 00:16:50,279 there. These things are trivially true. 502 00:16:50,280 --> 00:16:52,019 Twenty three equals twenty three yaara. 503 00:16:52,020 --> 00:16:54,119 And this is the proof for 504 00:16:54,120 --> 00:16:56,099 it. So when we want to prove that two 505 00:16:56,100 --> 00:16:58,319 things are true, just give 506 00:16:58,320 --> 00:17:00,239 me two proofs, give me the two proofs and 507 00:17:00,240 --> 00:17:01,289 put them together in Sabal. 508 00:17:03,630 --> 00:17:05,699 So whereas n there is 509 00:17:05,700 --> 00:17:07,949 or we've got something 510 00:17:07,950 --> 00:17:09,299 that's called the either type or some 511 00:17:09,300 --> 00:17:11,368 type, in this case it takes 512 00:17:11,369 --> 00:17:13,469 to type arguments and it has to 513 00:17:13,470 --> 00:17:15,539 constructors either a constructor for 514 00:17:15,540 --> 00:17:18,118 the left type which say or a constructor 515 00:17:18,119 --> 00:17:19,019 for the right. 516 00:17:19,020 --> 00:17:21,088 It says it's attacked union 517 00:17:21,089 --> 00:17:22,318 if you like to say that. 518 00:17:22,319 --> 00:17:24,299 So another example. 519 00:17:24,300 --> 00:17:26,519 This is obviously true and this isn't. 520 00:17:26,520 --> 00:17:28,259 But we've got a proof for this 521 00:17:28,260 --> 00:17:30,119 proposition because we can construct this 522 00:17:30,120 --> 00:17:32,369 value like an OR 523 00:17:32,370 --> 00:17:34,469 if one of these things is 524 00:17:34,470 --> 00:17:36,299 true, then we can construct the whole 525 00:17:36,300 --> 00:17:37,409 value. 526 00:17:37,410 --> 00:17:39,509 And this leads 527 00:17:39,510 --> 00:17:41,849 to some very interesting conclusions 528 00:17:41,850 --> 00:17:43,619 with logic. When you've got the last 529 00:17:43,620 --> 00:17:45,959 exclude the excluded middle, 530 00:17:45,960 --> 00:17:48,149 where you got every proposition, P, P 531 00:17:48,150 --> 00:17:49,919 or not P is always true. 532 00:17:49,920 --> 00:17:51,989 That's a problem because 533 00:17:51,990 --> 00:17:53,430 there are unsolved problems. 534 00:17:54,570 --> 00:17:56,699 People's enpi true or not 535 00:17:56,700 --> 00:17:57,899 true. 536 00:17:57,900 --> 00:17:59,909 Wycheproof, we don't know, we can't 537 00:17:59,910 --> 00:18:01,889 provide a proof because we don't have a 538 00:18:01,890 --> 00:18:04,079 proof for it and we have not we 539 00:18:04,080 --> 00:18:05,359 don't even have a reputation, 540 00:18:06,540 --> 00:18:08,129 so that's a problem and we are going to 541 00:18:08,130 --> 00:18:09,130 deal with that. 542 00:18:10,740 --> 00:18:13,709 So next thing, implication, 543 00:18:13,710 --> 00:18:15,839 so when I've got a proof of something, 544 00:18:15,840 --> 00:18:18,269 I can transform it into another proof. 545 00:18:18,270 --> 00:18:20,399 So this is once again, this is very, 546 00:18:20,400 --> 00:18:22,349 very trivial example. 547 00:18:22,350 --> 00:18:24,659 So when A is true, it implies 548 00:18:24,660 --> 00:18:25,890 that is true. Big deal. 549 00:18:27,600 --> 00:18:29,489 And this is what this type signature 550 00:18:29,490 --> 00:18:31,679 says. It's a very trivial 551 00:18:31,680 --> 00:18:33,749 theorem, but it's it's 552 00:18:33,750 --> 00:18:35,429 a theorem of less. 553 00:18:35,430 --> 00:18:37,739 So this thing over 554 00:18:37,740 --> 00:18:39,899 there is just a lambda. 555 00:18:39,900 --> 00:18:41,459 If you know JavaScript, it's when you 556 00:18:41,460 --> 00:18:44,009 write function, Perens, EXPAREL, 557 00:18:44,010 --> 00:18:45,629 yada, yada, lots of stuff. 558 00:18:45,630 --> 00:18:46,569 We just write backslash. 559 00:18:46,570 --> 00:18:48,149 We thought it was better than just 560 00:18:48,150 --> 00:18:49,150 writing function. 561 00:18:50,880 --> 00:18:52,050 So here we're using that. 562 00:18:53,280 --> 00:18:55,409 Pretty simple. Once again, you might 563 00:18:55,410 --> 00:18:57,479 notice that we're not stating a 564 00:18:57,480 --> 00:18:58,499 as a type argument. 565 00:18:58,500 --> 00:18:59,909 That is it. 566 00:18:59,910 --> 00:19:01,199 We can figure that out. I was a little 567 00:19:01,200 --> 00:19:03,449 bit while noisy in the first 568 00:19:03,450 --> 00:19:05,610 example. So here you go. 569 00:19:07,860 --> 00:19:09,479 So now it's getting weird, now we're 570 00:19:09,480 --> 00:19:11,279 getting into the penalty phase plan, 571 00:19:11,280 --> 00:19:12,659 since we want to have something like a 572 00:19:12,660 --> 00:19:13,769 predicate logic, we want to have 573 00:19:13,770 --> 00:19:16,289 quantification, universal quantification 574 00:19:16,290 --> 00:19:17,609 or quantification. 575 00:19:17,610 --> 00:19:20,219 And this is the new universal case. 576 00:19:20,220 --> 00:19:22,469 So it's just a generalization 577 00:19:22,470 --> 00:19:24,299 of the function space. 578 00:19:24,300 --> 00:19:26,429 So here, the 579 00:19:26,430 --> 00:19:28,529 return type actually depends 580 00:19:28,530 --> 00:19:30,149 on the value that we feed into the 581 00:19:30,150 --> 00:19:31,150 function. 582 00:19:32,580 --> 00:19:34,889 So this you can read this one is for 583 00:19:34,890 --> 00:19:37,169 all natural numbers, we can say 584 00:19:37,170 --> 00:19:39,179 one plus and equals and plus one. 585 00:19:39,180 --> 00:19:41,009 That might sound trivial, but we need 586 00:19:41,010 --> 00:19:44,579 proof that it's mathematics. 587 00:19:44,580 --> 00:19:46,529 So natural numbers are defined 588 00:19:46,530 --> 00:19:47,489 inductively. 589 00:19:47,490 --> 00:19:50,609 It's either a zero or a successor. 590 00:19:50,610 --> 00:19:52,709 So in the zero case we can say, 591 00:19:52,710 --> 00:19:54,999 OK, we can fill in zero. 592 00:19:55,000 --> 00:19:57,209 Are there we we see one equals 593 00:19:57,210 --> 00:19:59,879 one. OK, reflexivity with one. 594 00:19:59,880 --> 00:20:02,069 Next thing we Panorama's on the next 595 00:20:02,070 --> 00:20:04,199 case along using here 596 00:20:04,200 --> 00:20:06,449 is calling plus s recursively 597 00:20:06,450 --> 00:20:08,279 and I'm using rewrite to rewrite the 598 00:20:08,280 --> 00:20:09,189 goal. 599 00:20:09,190 --> 00:20:10,139 It's not that important. 600 00:20:10,140 --> 00:20:12,029 I can show it to you after the talk, but 601 00:20:12,030 --> 00:20:13,209 we're not going to into depth. 602 00:20:13,210 --> 00:20:15,479 So this is a proof by induction. 603 00:20:15,480 --> 00:20:18,119 So the stuff you learn at school 604 00:20:18,120 --> 00:20:19,919 and I never understand in school, but I 605 00:20:19,920 --> 00:20:21,479 understand with different types what 606 00:20:21,480 --> 00:20:22,739 word. 607 00:20:22,740 --> 00:20:24,869 So it feels natural. 608 00:20:24,870 --> 00:20:25,870 I don't know. 609 00:20:27,030 --> 00:20:28,589 So just for the sake of completeness, 610 00:20:28,590 --> 00:20:30,059 we've got existential quantification. 611 00:20:30,060 --> 00:20:31,529 We are not going to talk about that. 612 00:20:31,530 --> 00:20:33,599 But I just want to fill you in on the 613 00:20:33,600 --> 00:20:35,789 stuff. Um, so 614 00:20:35,790 --> 00:20:37,259 recall the vector. 615 00:20:37,260 --> 00:20:39,599 The vector has length of 616 00:20:39,600 --> 00:20:42,419 some natural number and 617 00:20:42,420 --> 00:20:44,639 when we filter that, so we've got a 618 00:20:44,640 --> 00:20:47,009 boolean function here that looks 619 00:20:47,010 --> 00:20:48,779 at every value and figures out this is 620 00:20:48,780 --> 00:20:51,089 true or false and we throw 621 00:20:51,090 --> 00:20:53,369 out elements if there are false. 622 00:20:53,370 --> 00:20:55,529 So we don't know what the lengths, but 623 00:20:55,530 --> 00:20:58,469 we know there exists some natural number 624 00:20:58,470 --> 00:20:59,789 that reflects that length. 625 00:21:01,850 --> 00:21:03,979 We use this kind of weird Tupperware, 626 00:21:03,980 --> 00:21:05,509 it's called, some people call this a 627 00:21:05,510 --> 00:21:06,510 dependent couple. 628 00:21:07,270 --> 00:21:09,139 Some people call it a dependent product. 629 00:21:09,140 --> 00:21:10,219 Some people call that independence. 630 00:21:10,220 --> 00:21:12,529 Some it's horribly confusing. 631 00:21:12,530 --> 00:21:13,819 I like to call them signal type. 632 00:21:15,650 --> 00:21:18,169 Yeah, very helpful. 633 00:21:18,170 --> 00:21:19,170 So, yeah, 634 00:21:20,510 --> 00:21:22,529 this is just we can say, OK, we can 635 00:21:22,530 --> 00:21:24,799 filter this and we know that there exists 636 00:21:24,800 --> 00:21:25,639 some length. 637 00:21:25,640 --> 00:21:27,889 If we filter VMT, it's obviously 638 00:21:27,890 --> 00:21:29,149 going to be the empty list. 639 00:21:29,150 --> 00:21:31,519 But if we filter some cons 640 00:21:31,520 --> 00:21:33,949 case, then we call filter recursively 641 00:21:33,950 --> 00:21:35,539 and we go through it. 642 00:21:35,540 --> 00:21:37,669 Either this is true, then 643 00:21:37,670 --> 00:21:40,129 we increment the length by one, otherwise 644 00:21:40,130 --> 00:21:42,199 we just throw it away and we don't keep 645 00:21:42,200 --> 00:21:43,729 track of that. 646 00:21:43,730 --> 00:21:45,199 So this type text as well. 647 00:21:47,150 --> 00:21:49,309 So last thing, I hope 648 00:21:49,310 --> 00:21:51,979 I'm not bothering you. So, um, 649 00:21:51,980 --> 00:21:53,179 so this is negation. 650 00:21:53,180 --> 00:21:54,589 We want to say when something is not 651 00:21:54,590 --> 00:21:56,689 true, obviously two equals 652 00:21:56,690 --> 00:21:59,089 three is not 653 00:21:59,090 --> 00:22:00,289 true. Yeah. 654 00:22:01,610 --> 00:22:04,009 So here 655 00:22:04,010 --> 00:22:06,439 unconvincing it that this is not possible 656 00:22:06,440 --> 00:22:08,359 when I'm saying OK, refl. 657 00:22:08,360 --> 00:22:09,589 This doesn't work. 658 00:22:09,590 --> 00:22:11,619 REFL is not a constructor of of two. 659 00:22:11,620 --> 00:22:12,559 Exactly. 660 00:22:12,560 --> 00:22:14,269 So we have to convince Esdras at some 661 00:22:14,270 --> 00:22:16,409 point that this is not going to work. 662 00:22:16,410 --> 00:22:18,380 So this impossible keyword helps. 663 00:22:20,390 --> 00:22:22,279 So whenever we are trying to say that 664 00:22:22,280 --> 00:22:24,409 something's not true or negate something, 665 00:22:24,410 --> 00:22:27,229 we just say that this proposition 666 00:22:27,230 --> 00:22:29,119 implies faults. 667 00:22:29,120 --> 00:22:30,499 So it's a function. 668 00:22:30,500 --> 00:22:32,719 So we have to map every value 669 00:22:32,720 --> 00:22:35,659 in the starting set to a value 670 00:22:35,660 --> 00:22:37,549 and in the in the image. 671 00:22:38,760 --> 00:22:39,760 Yeah. 672 00:22:39,920 --> 00:22:40,920 So 673 00:22:41,990 --> 00:22:44,119 if, if the domain is empty 674 00:22:44,120 --> 00:22:46,609 then we can't map it 675 00:22:46,610 --> 00:22:48,919 then, then we can map every point. 676 00:22:48,920 --> 00:22:51,079 But if the domain is not empty and the 677 00:22:51,080 --> 00:22:53,359 domain is empty, we've got a problem 678 00:22:53,360 --> 00:22:54,619 because we kind of map these types. 679 00:22:54,620 --> 00:22:56,029 We cannot do this function. 680 00:22:56,030 --> 00:22:58,219 So this is what this negation 681 00:22:58,220 --> 00:22:59,220 stuff is about. 682 00:23:00,380 --> 00:23:02,089 And now we're going to use that. 683 00:23:02,090 --> 00:23:03,589 As I said before, the Law of the Excluded 684 00:23:03,590 --> 00:23:05,719 Middle says that every 685 00:23:05,720 --> 00:23:08,839 proposition is either true or not true, 686 00:23:08,840 --> 00:23:10,459 which is a problem when we've got of 687 00:23:10,460 --> 00:23:11,389 problems. 688 00:23:11,390 --> 00:23:12,390 So. 689 00:23:12,870 --> 00:23:15,169 We want to negate that, we would just say 690 00:23:15,170 --> 00:23:17,239 not this is not true, which 691 00:23:17,240 --> 00:23:19,129 would be a very big problem because then 692 00:23:19,130 --> 00:23:20,779 we couldn't decide, decide if something 693 00:23:20,780 --> 00:23:21,979 was true or not. 694 00:23:21,980 --> 00:23:24,049 So we in this case, we're saying not 695 00:23:24,050 --> 00:23:26,299 not. And that's not the classical not 696 00:23:26,300 --> 00:23:28,039 not in classical logic. 697 00:23:28,040 --> 00:23:29,809 Not not a is a. 698 00:23:29,810 --> 00:23:31,939 So this is not 699 00:23:31,940 --> 00:23:33,829 it's not that way in constructive logic. 700 00:23:33,830 --> 00:23:36,169 So what this is saying is say we do not 701 00:23:36,170 --> 00:23:38,749 refute the law of the excluded middle. 702 00:23:38,750 --> 00:23:41,299 We cannot assume it in general, 703 00:23:41,300 --> 00:23:43,009 which is a very important distinction. 704 00:23:44,300 --> 00:23:46,599 So this 705 00:23:46,600 --> 00:23:48,410 either A not a is 706 00:23:49,880 --> 00:23:52,129 so popular that we got 707 00:23:52,130 --> 00:23:53,809 it's on tape. 708 00:23:53,810 --> 00:23:55,879 We call it deck for the Citable, and we 709 00:23:55,880 --> 00:23:58,010 will use that in the same sample. 710 00:23:59,120 --> 00:24:01,099 So life quoting once we fail. 711 00:24:04,250 --> 00:24:05,389 So let's try a new model. 712 00:24:05,390 --> 00:24:06,390 We call this demo. 713 00:24:07,520 --> 00:24:10,069 And yeah. 714 00:24:10,070 --> 00:24:12,289 So I want to introduce you to a 715 00:24:12,290 --> 00:24:13,290 nice little 716 00:24:14,570 --> 00:24:16,939 data structure, which is called Free. 717 00:24:16,940 --> 00:24:17,940 And it takes a type 718 00:24:19,340 --> 00:24:21,109 and it turns out. 719 00:24:21,110 --> 00:24:23,299 So it's got to constructor's got a leaf 720 00:24:23,300 --> 00:24:24,499 and branch. 721 00:24:24,500 --> 00:24:26,240 So tree of a 722 00:24:27,290 --> 00:24:29,449 branch and it takes 723 00:24:29,450 --> 00:24:31,789 a value of eight, takes the left hand 724 00:24:31,790 --> 00:24:34,069 tree and the right tree and 725 00:24:34,070 --> 00:24:35,070 returns the tree. 726 00:24:36,080 --> 00:24:37,080 So. 727 00:24:39,870 --> 00:24:42,239 So this type takes so we can 728 00:24:42,240 --> 00:24:44,399 type check this in them, if 729 00:24:44,400 --> 00:24:46,079 you're using IMEX, there is a great emacs 730 00:24:46,080 --> 00:24:47,080 mode, 731 00:24:49,680 --> 00:24:52,379 so everyone served here, 732 00:24:52,380 --> 00:24:53,380 so. 733 00:24:54,390 --> 00:24:55,619 Oh, excuse me. 734 00:24:56,930 --> 00:24:59,449 And as we just have to 735 00:24:59,450 --> 00:25:00,469 just have to leave. 736 00:25:00,470 --> 00:25:02,809 It's just a leaf leaf 737 00:25:02,810 --> 00:25:04,969 ranch, leaf ranch, whatever, so 738 00:25:04,970 --> 00:25:06,859 you can take an empty tree is just a 739 00:25:06,860 --> 00:25:07,860 leaf. 740 00:25:14,020 --> 00:25:15,550 Whatever, yeah, 741 00:25:17,980 --> 00:25:20,259 value, yes, 742 00:25:20,260 --> 00:25:21,759 it doesn't have a value level, we can 743 00:25:21,760 --> 00:25:24,519 think of it as a liability, so 744 00:25:24,520 --> 00:25:25,839 let's build something that we can live 745 00:25:25,840 --> 00:25:28,029 with and we've 746 00:25:28,030 --> 00:25:30,399 got a function from A to B to C, 747 00:25:30,400 --> 00:25:33,819 and it takes a tree of A.P. 748 00:25:33,820 --> 00:25:36,519 and returns a tree of C, 749 00:25:36,520 --> 00:25:38,799 so we put them on top of each other and 750 00:25:38,800 --> 00:25:41,019 just well, apply 751 00:25:41,020 --> 00:25:42,300 the function to all the Paris. 752 00:25:43,570 --> 00:25:44,570 So, yeah. 753 00:25:45,420 --> 00:25:47,429 I can say, give me a definition, so this 754 00:25:47,430 --> 00:25:49,229 is one of the this is the interactive 755 00:25:49,230 --> 00:25:51,299 stuff that I was talking 756 00:25:51,300 --> 00:25:53,459 about, need to do 757 00:25:53,460 --> 00:25:55,439 something and it will help the compiler a 758 00:25:55,440 --> 00:25:56,440 little bit here. 759 00:25:58,860 --> 00:25:59,860 Excuse me. 760 00:26:00,900 --> 00:26:02,999 So there's be so I'm 761 00:26:03,000 --> 00:26:04,409 just telling you this. 762 00:26:04,410 --> 00:26:06,539 Please choose these names because it is 763 00:26:06,540 --> 00:26:07,829 terrible at choosing names. 764 00:26:09,330 --> 00:26:10,679 It's horrible, really. 765 00:26:10,680 --> 00:26:12,659 Trust me. So what I can do now is I can 766 00:26:12,660 --> 00:26:13,709 do pattern matching. 767 00:26:13,710 --> 00:26:15,989 I can, but in 768 00:26:15,990 --> 00:26:17,789 this case I can do case splitting. 769 00:26:17,790 --> 00:26:19,949 So give me all the cases that you 770 00:26:19,950 --> 00:26:20,950 want, can have 771 00:26:22,020 --> 00:26:24,099 it and can have two cases, can have 772 00:26:24,100 --> 00:26:26,159 a leaf or branch. 773 00:26:26,160 --> 00:26:26,999 So yeah. Cool. 774 00:26:27,000 --> 00:26:29,639 Let's keep going. 775 00:26:29,640 --> 00:26:31,619 So careful. 776 00:26:31,620 --> 00:26:32,620 OK, this works 777 00:26:33,960 --> 00:26:35,249 ok. 778 00:26:35,250 --> 00:26:37,589 These things are called holds 779 00:26:37,590 --> 00:26:38,819 on metal variables. 780 00:26:38,820 --> 00:26:40,559 It's a part of the program that we didn't 781 00:26:40,560 --> 00:26:43,169 write yet and we can ask address 782 00:26:43,170 --> 00:26:45,629 are what type does it have. 783 00:26:45,630 --> 00:26:47,130 So this is what we know. 784 00:26:48,270 --> 00:26:49,679 We know these things. 785 00:26:49,680 --> 00:26:50,680 This is where we want to get. 786 00:26:52,230 --> 00:26:54,299 So can I can 787 00:26:54,300 --> 00:26:56,489 ask Idriz, can you solve this problem, 788 00:26:56,490 --> 00:26:57,689 can solve that for me? 789 00:26:57,690 --> 00:26:59,759 And in this case it could. 790 00:26:59,760 --> 00:27:02,009 But what happens 791 00:27:02,010 --> 00:27:04,889 if we got this case so 792 00:27:04,890 --> 00:27:06,359 we can throw away data? 793 00:27:06,360 --> 00:27:08,639 That might be the tactic 794 00:27:08,640 --> 00:27:09,929 that we want to use in some cases. 795 00:27:09,930 --> 00:27:11,519 But in other cases, that might be bad 796 00:27:11,520 --> 00:27:13,079 because we are losing information. 797 00:27:13,080 --> 00:27:14,519 We don't want to have that. 798 00:27:14,520 --> 00:27:16,589 So this is this is 799 00:27:16,590 --> 00:27:17,789 kind of bad. 800 00:27:17,790 --> 00:27:18,719 We don't want that. 801 00:27:18,720 --> 00:27:21,899 We don't want these two cases to happen. 802 00:27:21,900 --> 00:27:24,389 So because we're we're losing information 803 00:27:24,390 --> 00:27:25,469 here. 804 00:27:25,470 --> 00:27:26,879 So what I'm going to do is I'm going to 805 00:27:26,880 --> 00:27:29,909 introduce a new type, 806 00:27:29,910 --> 00:27:31,079 which is tree shape. 807 00:27:33,720 --> 00:27:34,720 And it's just the type 808 00:27:35,820 --> 00:27:37,349 and that's called this a leaf shape, 809 00:27:38,490 --> 00:27:40,739 which is a tree shape and the branch 810 00:27:40,740 --> 00:27:41,740 shape 811 00:27:42,900 --> 00:27:43,900 which takes the tree shape 812 00:27:45,870 --> 00:27:47,549 and reshape. 813 00:27:47,550 --> 00:27:49,829 And so this is the shape 814 00:27:49,830 --> 00:27:51,119 of the left and right branch. 815 00:27:52,320 --> 00:27:53,790 Let's throw this one away 816 00:27:55,170 --> 00:27:56,700 and take a tree shape here. 817 00:28:00,210 --> 00:28:02,579 So this is obviously 818 00:28:02,580 --> 00:28:04,649 we think this has some 819 00:28:04,650 --> 00:28:06,779 shape as some shape 820 00:28:06,780 --> 00:28:08,999 as prime, and it will take 821 00:28:09,000 --> 00:28:11,309 a branch shape of 822 00:28:11,310 --> 00:28:12,310 S in its prime. 823 00:28:15,000 --> 00:28:17,269 So once again, that 824 00:28:17,270 --> 00:28:18,270 was 825 00:28:19,420 --> 00:28:20,420 see, 826 00:28:21,750 --> 00:28:22,750 so 827 00:28:25,260 --> 00:28:27,299 now I'm assuming that these trees are 828 00:28:27,300 --> 00:28:29,099 going to have the same shape. 829 00:28:29,100 --> 00:28:30,730 Oh, this is wrong. 830 00:28:32,140 --> 00:28:34,259 This OK, 831 00:28:34,260 --> 00:28:36,119 obviously this type Czechia. 832 00:28:36,120 --> 00:28:37,319 That's nice. 833 00:28:37,320 --> 00:28:39,869 So now we can explain 834 00:28:39,870 --> 00:28:41,969 once again, kispert 835 00:28:41,970 --> 00:28:43,859 here, split there. 836 00:28:43,860 --> 00:28:44,860 And lo and behold. 837 00:28:47,230 --> 00:28:48,549 The other cases, they don't show up 838 00:28:48,550 --> 00:28:50,739 anymore because it was figured out 839 00:28:50,740 --> 00:28:52,180 if this one belief, 840 00:28:53,350 --> 00:28:55,449 then this has to be a life as well. 841 00:28:55,450 --> 00:28:57,820 Same goes for the branch because 842 00:28:58,870 --> 00:29:00,999 they all got the same shape we 843 00:29:01,000 --> 00:29:03,339 statically and guaranteed 844 00:29:03,340 --> 00:29:05,409 that these safes got to be 845 00:29:05,410 --> 00:29:06,410 the same. 846 00:29:06,910 --> 00:29:08,709 So now this this is getting pretty nice. 847 00:29:08,710 --> 00:29:10,629 So in Haskell, you've got something 848 00:29:10,630 --> 00:29:12,429 that's called type inference where you 849 00:29:12,430 --> 00:29:14,559 can write program and 850 00:29:14,560 --> 00:29:16,629 Housel can infer the type. 851 00:29:16,630 --> 00:29:18,279 We can't do that independently type 852 00:29:18,280 --> 00:29:20,389 language, but we can do something else. 853 00:29:20,390 --> 00:29:22,359 You can say write this program. 854 00:29:22,360 --> 00:29:24,429 It was it 855 00:29:24,430 --> 00:29:26,889 was said, OK, that's we 856 00:29:26,890 --> 00:29:29,649 can do this. This looks pretty tricky. 857 00:29:29,650 --> 00:29:30,969 Yes, it can do that. 858 00:29:30,970 --> 00:29:32,739 So this is pretty neat 859 00:29:34,180 --> 00:29:35,709 once we've got enough information that 860 00:29:35,710 --> 00:29:36,710 high level. 861 00:29:43,300 --> 00:29:45,129 Yes, I can sympathize. 862 00:29:45,130 --> 00:29:46,449 This blew me out of the water when I saw 863 00:29:46,450 --> 00:29:48,909 it first. This is so 864 00:29:48,910 --> 00:29:51,129 great work. Everyone does 865 00:29:51,130 --> 00:29:51,949 even better at that. 866 00:29:51,950 --> 00:29:54,669 But yeah, so 867 00:29:54,670 --> 00:29:57,099 it can figure out 868 00:29:57,100 --> 00:29:58,749 by the information that it's got there 869 00:29:59,950 --> 00:30:01,119 so we can look at that. 870 00:30:01,120 --> 00:30:02,739 So it's a lot of information, but I've 871 00:30:02,740 --> 00:30:04,719 written this by hand, but we don't need 872 00:30:04,720 --> 00:30:05,659 it. 873 00:30:05,660 --> 00:30:07,299 That's pretty nice. 874 00:30:08,800 --> 00:30:10,959 So let's let's prove something. 875 00:30:10,960 --> 00:30:13,479 Let's, let's write a function and 876 00:30:13,480 --> 00:30:15,459 we call this one is Ellem and we want to 877 00:30:15,460 --> 00:30:17,559 check if an element is in 878 00:30:17,560 --> 00:30:18,560 the tree. 879 00:30:19,060 --> 00:30:21,219 And I'm going to gloss over this 880 00:30:21,220 --> 00:30:23,139 detail for a second. 881 00:30:23,140 --> 00:30:24,879 So bear with me, please. 882 00:30:24,880 --> 00:30:27,219 So we've got some element of X 883 00:30:27,220 --> 00:30:28,239 of Type A. 884 00:30:28,240 --> 00:30:30,339 We've got a treaty which has some 885 00:30:30,340 --> 00:30:32,589 say it asks and it has elements 886 00:30:32,590 --> 00:30:34,359 of it. So what? 887 00:30:34,360 --> 00:30:36,469 So what could be the 888 00:30:36,470 --> 00:30:38,529 the result type that we 889 00:30:38,530 --> 00:30:40,629 want here in in a 890 00:30:40,630 --> 00:30:42,219 lot of languages, we say, OK, this is a 891 00:30:42,220 --> 00:30:44,289 boolean, but that's a 892 00:30:44,290 --> 00:30:46,299 little bit problematic because a boolean 893 00:30:46,300 --> 00:30:48,009 doesn't really convey any information. 894 00:30:48,010 --> 00:30:50,409 It's just it's just saying yes or no. 895 00:30:50,410 --> 00:30:53,049 It's like the answer is forty two. 896 00:30:53,050 --> 00:30:54,050 What's the question? 897 00:30:55,030 --> 00:30:56,889 It's not very helpful. 898 00:30:56,890 --> 00:31:00,009 So what I want to do now 899 00:31:00,010 --> 00:31:02,739 is I want to write 900 00:31:02,740 --> 00:31:05,259 a predicate that contains 901 00:31:05,260 --> 00:31:06,609 a lot more information than just the 902 00:31:06,610 --> 00:31:07,779 boolean. 903 00:31:07,780 --> 00:31:09,189 In the case of the Boolean, I could just 904 00:31:09,190 --> 00:31:11,409 write false for every case so I could 905 00:31:11,410 --> 00:31:13,149 write a wrong function here. 906 00:31:14,620 --> 00:31:16,839 So let's write a predicate. 907 00:31:16,840 --> 00:31:18,909 We call this is Ellum 908 00:31:18,910 --> 00:31:19,910 and 909 00:31:21,790 --> 00:31:22,790 it looks like this. 910 00:31:24,190 --> 00:31:26,289 So let me 911 00:31:26,290 --> 00:31:27,290 look at my church here 912 00:31:30,400 --> 00:31:32,769 x the branch 913 00:31:34,120 --> 00:31:36,009 and the left and the right tree. 914 00:31:36,010 --> 00:31:38,169 So this is a proof that we found the 915 00:31:38,170 --> 00:31:39,369 element. 916 00:31:39,370 --> 00:31:41,649 So we're not 917 00:31:41,650 --> 00:31:43,929 saying this is we're not just saying, OK, 918 00:31:43,930 --> 00:31:45,759 we found the element, but we are 919 00:31:45,760 --> 00:31:48,049 constructing a path to find this element. 920 00:31:49,090 --> 00:31:50,949 So this is the proof that we found it. 921 00:31:50,950 --> 00:31:52,690 Obviously, we need are 922 00:31:54,580 --> 00:31:55,899 the paths. 923 00:31:55,900 --> 00:31:58,689 So if we know that 924 00:31:58,690 --> 00:32:01,090 is X is in the left branch, 925 00:32:02,320 --> 00:32:03,579 then we can say 926 00:32:04,930 --> 00:32:06,339 it's in. 927 00:32:08,910 --> 00:32:09,910 This tree. 928 00:32:12,680 --> 00:32:14,869 Oh, what are you doing 929 00:32:14,870 --> 00:32:15,870 there, 930 00:32:17,660 --> 00:32:18,660 telling me 931 00:32:21,150 --> 00:32:23,219 it again, unexpected and 932 00:32:23,220 --> 00:32:24,220 food, 933 00:32:26,630 --> 00:32:27,979 what is so er. 934 00:32:27,980 --> 00:32:28,980 Yeah 935 00:32:30,530 --> 00:32:32,629 so say hello 936 00:32:32,630 --> 00:32:33,630 to the type again 937 00:32:38,210 --> 00:32:41,179 so we can decide this problem 938 00:32:41,180 --> 00:32:43,459 can say for all elements 939 00:32:43,460 --> 00:32:45,589 of type A, for some tree we 940 00:32:45,590 --> 00:32:48,199 can decide if the element is in there. 941 00:32:48,200 --> 00:32:49,849 This is why, this is why I introduced the 942 00:32:49,850 --> 00:32:51,409 deck type anyway. 943 00:32:51,410 --> 00:32:52,410 So 944 00:32:55,310 --> 00:32:56,750 obviously we need the right 945 00:32:58,160 --> 00:32:59,160 content 946 00:33:00,590 --> 00:33:03,099 so yes 947 00:33:08,870 --> 00:33:09,799 please. Type. 948 00:33:09,800 --> 00:33:10,800 Yeah. 949 00:33:11,580 --> 00:33:12,580 Yeah. 950 00:33:15,690 --> 00:33:17,599 We get to the later, OK? 951 00:33:17,600 --> 00:33:19,799 Can can can an element be in a leaf? 952 00:33:19,800 --> 00:33:20,880 So look at the constructor. 953 00:33:24,030 --> 00:33:25,710 No, it can't. 954 00:33:27,030 --> 00:33:28,499 So the branch 955 00:33:30,530 --> 00:33:31,509 you can. A branch. 956 00:33:31,510 --> 00:33:33,809 Yeah. The leaf doesn't have an element. 957 00:33:33,810 --> 00:33:35,309 That's what I meant with empty tree. 958 00:33:35,310 --> 00:33:36,539 It doesn't have any elements in this 959 00:33:36,540 --> 00:33:37,540 case. 960 00:33:39,870 --> 00:33:42,030 Now, it'll be a little bit smaller here. 961 00:33:46,290 --> 00:33:48,389 Yeah. Because of the tree of a 962 00:33:48,390 --> 00:33:50,069 leaf and the leaf. 963 00:33:50,070 --> 00:33:52,439 But yeah, because it's a tree of a 964 00:33:52,440 --> 00:33:53,970 but it doesn't have any elements. 965 00:33:55,710 --> 00:33:56,710 Yeah. 966 00:33:57,770 --> 00:33:59,959 It's an empty it's an empty 967 00:33:59,960 --> 00:34:02,419 tree of type A, 968 00:34:02,420 --> 00:34:03,420 whatever is. 969 00:34:06,370 --> 00:34:07,370 So it's split here 970 00:34:09,580 --> 00:34:11,559 and let's find out. 971 00:34:13,159 --> 00:34:14,969 What is what we want here? 972 00:34:16,280 --> 00:34:18,289 So obviously there cannot be an element 973 00:34:18,290 --> 00:34:20,089 in this in this thing because Leif 974 00:34:20,090 --> 00:34:22,279 doesn't have any values in there. 975 00:34:22,280 --> 00:34:24,709 So what I'm going to right now is. 976 00:34:28,870 --> 00:34:31,089 A function that says 977 00:34:31,090 --> 00:34:33,459 not in life, 978 00:34:33,460 --> 00:34:35,529 so yeah, and 979 00:34:35,530 --> 00:34:36,599 I'm going to extract the Lamba, 980 00:34:37,840 --> 00:34:39,968 so let me 981 00:34:39,969 --> 00:34:41,529 get rid of this. 982 00:34:41,530 --> 00:34:43,340 Sometimes it was very 983 00:34:47,050 --> 00:34:48,549 just wants to add a lot a lot of 984 00:34:48,550 --> 00:34:49,550 arguments. 985 00:34:50,409 --> 00:34:53,109 OK, let's just to you, 986 00:34:53,110 --> 00:34:55,300 not in life 987 00:34:56,440 --> 00:34:58,159 excuse me here. 988 00:34:58,160 --> 00:34:59,360 And this is just impossible. 989 00:35:00,640 --> 00:35:02,769 This is this is once again, 990 00:35:02,770 --> 00:35:04,929 so in this case, 991 00:35:06,340 --> 00:35:07,989 this this this thing doesn't have any 992 00:35:07,990 --> 00:35:10,149 elements, therefore it cannot have 993 00:35:10,150 --> 00:35:11,229 X in it. 994 00:35:12,430 --> 00:35:14,859 So this proof 995 00:35:14,860 --> 00:35:15,860 says 996 00:35:17,080 --> 00:35:18,080 be in there. 997 00:35:21,610 --> 00:35:24,669 Ah, yeah, and tiebreaks, 998 00:35:24,670 --> 00:35:25,900 so we can right here. 999 00:35:27,130 --> 00:35:28,449 This is just the same thing, let's make 1000 00:35:28,450 --> 00:35:30,169 this a little prayer. 1001 00:35:30,170 --> 00:35:32,799 So now we've got to prove that 1002 00:35:32,800 --> 00:35:34,650 in a leaf there can be any elements. 1003 00:35:36,760 --> 00:35:38,769 So we've got a reputation for that. 1004 00:35:38,770 --> 00:35:39,770 So 1005 00:35:41,030 --> 00:35:43,059 to do something else. 1006 00:35:44,620 --> 00:35:46,089 Well, I'm going to do now is I'm going to 1007 00:35:46,090 --> 00:35:47,799 do something that's called a width 1008 00:35:47,800 --> 00:35:49,509 pattern, which is an intermediate 1009 00:35:49,510 --> 00:35:50,799 computation. 1010 00:35:50,800 --> 00:35:52,899 And now I'm going to use this 1011 00:35:52,900 --> 00:35:55,449 technique. So this is a type class 1012 00:35:55,450 --> 00:35:57,669 that says for type A, we can 1013 00:35:57,670 --> 00:35:59,559 decide if two things are equal. 1014 00:35:59,560 --> 00:36:01,749 So there are there are some things that 1015 00:36:01,750 --> 00:36:03,879 cannot we cannot prove to be equal. 1016 00:36:03,880 --> 00:36:06,099 It's a little bit bothersome, but, 1017 00:36:06,100 --> 00:36:07,100 yeah, they exist. 1018 00:36:09,430 --> 00:36:10,839 So we can explain once again, 1019 00:36:12,820 --> 00:36:13,479 once again. 1020 00:36:13,480 --> 00:36:14,769 And look at that. 1021 00:36:14,770 --> 00:36:15,770 So. 1022 00:36:17,890 --> 00:36:20,049 This is why and once I'm 1023 00:36:20,050 --> 00:36:21,219 doing pattern matching here. 1024 00:36:24,150 --> 00:36:26,609 It turns into acts, so it figured out 1025 00:36:26,610 --> 00:36:28,799 that these two elements got 1026 00:36:28,800 --> 00:36:30,599 to be the same because we've got a proof 1027 00:36:30,600 --> 00:36:31,949 of that. This is dependent pattern 1028 00:36:31,950 --> 00:36:34,309 matching or non-linear 1029 00:36:34,310 --> 00:36:35,279 matching. 1030 00:36:35,280 --> 00:36:37,409 So let's once again try to find proof 1031 00:36:37,410 --> 00:36:39,239 and here's a proof. 1032 00:36:39,240 --> 00:36:40,829 So writing these things is utterly 1033 00:36:40,830 --> 00:36:41,879 boring. 1034 00:36:41,880 --> 00:36:44,519 This is got this 1035 00:36:44,520 --> 00:36:46,860 written down somewhere. 1036 00:36:48,610 --> 00:36:50,639 So, yeah. This is oh, 1037 00:36:52,890 --> 00:36:55,859 so hot and loaded, 1038 00:36:55,860 --> 00:36:56,860 Volmer. 1039 00:37:03,460 --> 00:37:05,469 Hmm, that's just an address. 1040 00:37:06,610 --> 00:37:08,709 It's nothing interesting, really. 1041 00:37:09,790 --> 00:37:11,260 So sources address 1042 00:37:12,550 --> 00:37:13,659 31 simply 1043 00:37:15,510 --> 00:37:17,739 I said this is 1044 00:37:17,740 --> 00:37:18,740 this is 1045 00:37:20,170 --> 00:37:22,269 demised them your 1046 00:37:22,270 --> 00:37:23,169 family. 1047 00:37:23,170 --> 00:37:24,489 So this is the whole thing. 1048 00:37:24,490 --> 00:37:25,479 And I don't want to write that. 1049 00:37:25,480 --> 00:37:27,219 This is just utterly boring. 1050 00:37:28,720 --> 00:37:30,939 Most of it was right before it was right 1051 00:37:30,940 --> 00:37:32,049 for you. 1052 00:37:32,050 --> 00:37:34,179 So what we got here is we 1053 00:37:34,180 --> 00:37:36,279 got to prove that we didn't find the 1054 00:37:36,280 --> 00:37:38,499 value in the industry 1055 00:37:38,500 --> 00:37:40,959 if we didn't find a value, the left 1056 00:37:40,960 --> 00:37:42,759 left branch and we didn't find a value in 1057 00:37:42,760 --> 00:37:44,919 the right branch. And this is a proof 1058 00:37:44,920 --> 00:37:47,139 that it's now four minutes, 1059 00:37:47,140 --> 00:37:49,099 40, 50 minutes, OK? 1060 00:37:52,450 --> 00:37:54,409 So this is a proof that it's not under a 1061 00:37:54,410 --> 00:37:55,410 tree. So 1062 00:37:56,530 --> 00:37:57,469 that's what I told you. 1063 00:37:57,470 --> 00:37:59,529 It's a decided problem whether that 1064 00:37:59,530 --> 00:38:00,639 thing is under the tree or not. 1065 00:38:02,710 --> 00:38:05,349 So, yeah, that was life coding 1066 00:38:05,350 --> 00:38:06,579 and not wanting to talk a little bit 1067 00:38:06,580 --> 00:38:08,169 about effects. 1068 00:38:08,170 --> 00:38:10,449 So until now, we didn't do any side 1069 00:38:10,450 --> 00:38:12,519 effects. And if you know, Haskell, there 1070 00:38:12,520 --> 00:38:15,099 is this that m word 1071 00:38:15,100 --> 00:38:16,180 I'm not going to mention here. 1072 00:38:17,380 --> 00:38:19,869 People people tend to get scared 1073 00:38:19,870 --> 00:38:21,759 every time I say that. 1074 00:38:21,760 --> 00:38:22,760 So 1075 00:38:24,340 --> 00:38:25,869 we've got something that's called 1076 00:38:25,870 --> 00:38:27,249 algebraic effects. I don't know if that 1077 00:38:27,250 --> 00:38:28,590 sound less scary. I don't think so. 1078 00:38:30,070 --> 00:38:32,169 So this is a very dumb 1079 00:38:32,170 --> 00:38:34,239 program, but nevertheless, it has 1080 00:38:34,240 --> 00:38:36,699 some interesting things to tell us. 1081 00:38:36,700 --> 00:38:38,979 So up there, this 1082 00:38:38,980 --> 00:38:41,139 is a very horrible 1083 00:38:41,140 --> 00:38:43,629 looking type signature, but 1084 00:38:43,630 --> 00:38:45,309 that's in fact the type signature. 1085 00:38:45,310 --> 00:38:47,379 So when we write types that 1086 00:38:47,380 --> 00:38:49,119 are bigger than the problem programs, 1087 00:38:49,120 --> 00:38:51,489 sometimes that 1088 00:38:51,490 --> 00:38:53,649 feels kind of weird. But OK, so what 1089 00:38:53,650 --> 00:38:55,329 this notation says, 1090 00:38:56,410 --> 00:38:59,209 we've got two effects, 1091 00:38:59,210 --> 00:39:01,449 got IO and we've got standard 1092 00:39:01,450 --> 00:39:03,889 IO so we can use the file 1093 00:39:03,890 --> 00:39:06,009 effect to work with filesystem. 1094 00:39:06,010 --> 00:39:08,199 We can open files, read files, files, 1095 00:39:08,200 --> 00:39:09,200 whatever 1096 00:39:10,570 --> 00:39:12,369 standard. I always just write something 1097 00:39:12,370 --> 00:39:13,569 to the console. 1098 00:39:13,570 --> 00:39:14,619 Nothing special here. 1099 00:39:14,620 --> 00:39:16,989 And we can put them into this list 1100 00:39:16,990 --> 00:39:19,089 so we can have a very expressive 1101 00:39:19,090 --> 00:39:21,159 type type signature, this type section 1102 00:39:21,160 --> 00:39:22,899 which tells us what what can go on. 1103 00:39:22,900 --> 00:39:24,819 So in Haskell there is this I o type and 1104 00:39:24,820 --> 00:39:26,919 it can pretty much do everything so it 1105 00:39:26,920 --> 00:39:28,989 can communicate with the outside world 1106 00:39:28,990 --> 00:39:31,189 or calculate pide, your hard drive, 1107 00:39:31,190 --> 00:39:32,619 whatever. 1108 00:39:32,620 --> 00:39:34,779 So in this case we just know, 1109 00:39:34,780 --> 00:39:36,909 OK, it's finial, 1110 00:39:36,910 --> 00:39:39,459 they can do some stuff on the file system 1111 00:39:39,460 --> 00:39:41,919 and it can write to 1112 00:39:41,920 --> 00:39:43,989 write to the council or read from the 1113 00:39:43,990 --> 00:39:44,990 console. 1114 00:39:45,550 --> 00:39:46,550 So 1115 00:39:48,070 --> 00:39:50,439 this type signature has a very 1116 00:39:50,440 --> 00:39:51,440 interesting 1117 00:39:52,660 --> 00:39:54,939 if the Sultan has a very 1118 00:39:54,940 --> 00:39:57,099 interesting Tapson dysfunction open 1119 00:39:58,570 --> 00:40:00,669 recognize that if then 1120 00:40:00,670 --> 00:40:02,379 else on the type level. 1121 00:40:02,380 --> 00:40:04,479 And what it does is 1122 00:40:04,480 --> 00:40:07,179 actually figure this out is 1123 00:40:07,180 --> 00:40:09,939 could we open the file if yes. 1124 00:40:09,940 --> 00:40:11,979 Then we've got an open file handle, 1125 00:40:11,980 --> 00:40:13,719 otherwise we don't have one. 1126 00:40:15,040 --> 00:40:17,109 So this is what we want 1127 00:40:17,110 --> 00:40:18,489 to use, something like if it's on the 1128 00:40:18,490 --> 00:40:19,779 type level. 1129 00:40:19,780 --> 00:40:21,939 So if we look at this affects example 1130 00:40:21,940 --> 00:40:22,940 once again. 1131 00:40:23,690 --> 00:40:25,879 We are pattern matching on the result, 1132 00:40:26,880 --> 00:40:29,719 is this a successful operation 1133 00:40:29,720 --> 00:40:31,909 in this case? Yeah, I can read from it. 1134 00:40:33,050 --> 00:40:34,429 So let me try to compile that. 1135 00:40:42,380 --> 00:40:44,400 The effects that. 1136 00:40:49,680 --> 00:40:50,680 Takes a lot of time, 1137 00:40:52,270 --> 00:40:54,019 it does a lot of things, 1138 00:40:55,250 --> 00:40:57,349 and the complaints gets faster, so it 1139 00:40:57,350 --> 00:41:00,199 just reads in the first line of 1140 00:41:00,200 --> 00:41:02,689 of this program of of the source code. 1141 00:41:02,690 --> 00:41:04,819 So, yeah. 1142 00:41:04,820 --> 00:41:06,619 So what happens if we do something like 1143 00:41:06,620 --> 00:41:07,609 that? 1144 00:41:07,610 --> 00:41:08,719 We're not closing the file. 1145 00:41:11,120 --> 00:41:13,119 Try to combat that. 1146 00:41:13,120 --> 00:41:14,919 And I was complaining, it says it went 1147 00:41:14,920 --> 00:41:15,819 wrong. 1148 00:41:15,820 --> 00:41:18,069 Basically, we are working 1149 00:41:18,070 --> 00:41:19,779 on something that's called a reflection, 1150 00:41:19,780 --> 00:41:21,999 which makes this stuff readable, 1151 00:41:22,000 --> 00:41:24,009 but if you squint a little bit, you might 1152 00:41:24,010 --> 00:41:26,229 be able to read it or if you're 1153 00:41:26,230 --> 00:41:28,719 just using it for very long time. 1154 00:41:28,720 --> 00:41:31,989 But what this actually says, it's OK. 1155 00:41:31,990 --> 00:41:33,670 You promised me that. 1156 00:41:34,810 --> 00:41:37,359 This thing would be closed 1157 00:41:37,360 --> 00:41:39,399 once you want to leave the program. 1158 00:41:39,400 --> 00:41:40,279 I didn't do that. 1159 00:41:40,280 --> 00:41:42,399 So it's still an open file handle so we 1160 00:41:42,400 --> 00:41:44,559 can track the files are open 1161 00:41:44,560 --> 00:41:46,119 as one of these things that happened 1162 00:41:46,120 --> 00:41:47,469 quite a lot. Are you aware of the 1163 00:41:47,470 --> 00:41:49,239 database? And you just leave that open 1164 00:41:49,240 --> 00:41:51,189 and you run on file handles and your 1165 00:41:51,190 --> 00:41:53,469 application crashes and everyone's sad 1166 00:41:53,470 --> 00:41:54,470 and. 1167 00:41:55,150 --> 00:41:56,439 Yeah, so you can check that. 1168 00:41:56,440 --> 00:41:58,329 We can check that a compile time. 1169 00:41:58,330 --> 00:42:00,199 We could also do something like that. 1170 00:42:00,200 --> 00:42:02,259 We tried to 1171 00:42:02,260 --> 00:42:04,959 read from and from closed file. 1172 00:42:04,960 --> 00:42:07,029 So yeah, this is going to spit 1173 00:42:07,030 --> 00:42:09,219 something else out that you're probably 1174 00:42:09,220 --> 00:42:10,590 not able to read. I'm, 1175 00:42:11,650 --> 00:42:13,089 I can't do that as well. 1176 00:42:13,090 --> 00:42:14,799 So yeah. 1177 00:42:14,800 --> 00:42:15,800 So 1178 00:42:16,960 --> 00:42:17,980 this is pretty useful 1179 00:42:20,410 --> 00:42:22,719 and I want to show you something that is 1180 00:42:22,720 --> 00:42:24,879 even more useful, maybe not 1181 00:42:24,880 --> 00:42:28,239 too much, but so 1182 00:42:28,240 --> 00:42:31,119 this is a little demo that does 1183 00:42:31,120 --> 00:42:33,369 typed csv. 1184 00:42:33,370 --> 00:42:35,440 So we read in CSV 1185 00:42:36,940 --> 00:42:39,309 and look at the the schema, 1186 00:42:39,310 --> 00:42:41,499 just the header file and look at ok, 1187 00:42:41,500 --> 00:42:43,689 what, what columns do we have 1188 00:42:43,690 --> 00:42:45,999 and read that and 1189 00:42:46,000 --> 00:42:47,679 we do that at compile time. 1190 00:42:47,680 --> 00:42:49,809 So once we compile this program 1191 00:42:49,810 --> 00:42:52,119 it goes out, reads in the file, picks 1192 00:42:52,120 --> 00:42:54,459 out the the header and generates 1193 00:42:54,460 --> 00:42:55,839 a schema. 1194 00:42:55,840 --> 00:42:57,939 And what's interesting about that 1195 00:42:57,940 --> 00:42:58,940 is. 1196 00:43:01,960 --> 00:43:02,960 So. 1197 00:43:04,090 --> 00:43:05,530 Yeah, there's a spokesman, so. 1198 00:43:08,150 --> 00:43:10,339 So this says, OK, 1199 00:43:10,340 --> 00:43:12,709 reading the file, read and my CSFI 1200 00:43:13,760 --> 00:43:16,489 pick out the header, generate a schema, 1201 00:43:16,490 --> 00:43:18,589 call this one test schema, and 1202 00:43:18,590 --> 00:43:20,869 whenever we add a new 1203 00:43:20,870 --> 00:43:23,029 row to this and all, 1204 00:43:23,030 --> 00:43:24,889 we want to query that we've got compile 1205 00:43:24,890 --> 00:43:26,989 time guarantees that this value is 1206 00:43:26,990 --> 00:43:27,919 actually in the CSFI. 1207 00:43:27,920 --> 00:43:29,239 So we don't have to check. 1208 00:43:29,240 --> 00:43:30,240 This is in their. 1209 00:43:31,550 --> 00:43:33,049 This will always succeed. 1210 00:43:33,050 --> 00:43:34,789 I'm going a little bit over the top with 1211 00:43:34,790 --> 00:43:36,949 this because I'm also stating the 1212 00:43:36,950 --> 00:43:39,499 amount of rose that I'm reading in, which 1213 00:43:39,500 --> 00:43:41,479 is a little bit too much to be practical, 1214 00:43:41,480 --> 00:43:43,689 but it's just for fun. 1215 00:43:46,640 --> 00:43:48,560 So, yeah, let me show that to you. 1216 00:43:56,240 --> 00:43:57,240 So let's compare that. 1217 00:44:01,080 --> 00:44:02,159 That takes even longer. 1218 00:44:06,180 --> 00:44:07,919 Yeah, that took quite some time, 1219 00:44:09,840 --> 00:44:12,219 so, yeah, it's Siggie, it's German 1220 00:44:12,220 --> 00:44:13,220 Puckerman, I'm sorry. 1221 00:44:16,020 --> 00:44:17,729 So let me carry something else which 1222 00:44:17,730 --> 00:44:19,179 isn't there. 1223 00:44:19,180 --> 00:44:20,180 Don't me. It was. 1224 00:44:22,660 --> 00:44:24,759 Yeah, and say, OK, this is this 1225 00:44:24,760 --> 00:44:26,979 is not element of the scheme, we couldn't 1226 00:44:26,980 --> 00:44:27,980 solve that. 1227 00:44:29,470 --> 00:44:32,559 You might recognize this is something 1228 00:44:32,560 --> 00:44:33,560 which is 1229 00:44:34,720 --> 00:44:36,640 over here in 1230 00:44:37,990 --> 00:44:38,990 this album. 1231 00:44:40,510 --> 00:44:42,549 So this is this should look familiar 1232 00:44:42,550 --> 00:44:43,809 somehow. 1233 00:44:43,810 --> 00:44:44,810 And 1234 00:44:46,120 --> 00:44:47,589 that's pretty neat. 1235 00:44:47,590 --> 00:44:49,659 So this one this 1236 00:44:49,660 --> 00:44:51,759 line constructs such a proof 1237 00:44:51,760 --> 00:44:53,589 automatically. So we don't want to. 1238 00:44:53,590 --> 00:44:54,579 Right there. 1239 00:44:54,580 --> 00:44:56,379 There are there here. 1240 00:44:56,380 --> 00:44:58,479 That's that's a dumb task. 1241 00:44:58,480 --> 00:45:00,129 So that compiler can do that. 1242 00:45:01,480 --> 00:45:04,059 So this is what this process is doing. 1243 00:45:04,060 --> 00:45:06,249 So whenever we are looking up some field 1244 00:45:06,250 --> 00:45:08,679 F in some schema, 1245 00:45:08,680 --> 00:45:10,779 we just try to find the proof 1246 00:45:10,780 --> 00:45:12,269 that it's in there. 1247 00:45:12,270 --> 00:45:14,789 And then return the result. 1248 00:45:14,790 --> 00:45:16,949 So, yeah, ten minutes, 1249 00:45:16,950 --> 00:45:17,879 I think I'm done here. 1250 00:45:17,880 --> 00:45:20,429 So if you want to ask me questions, 1251 00:45:20,430 --> 00:45:21,430 please go ahead. 1252 00:45:34,880 --> 00:45:36,589 My mind is still blown, but if you have 1253 00:45:36,590 --> 00:45:38,029 questions lined up in front of the 1254 00:45:38,030 --> 00:45:40,339 microphone and ask 1255 00:45:40,340 --> 00:45:41,340 away, 1256 00:45:42,410 --> 00:45:43,520 let's grill the speaker, 1257 00:45:45,500 --> 00:45:47,809 microphone one, OK, so thank 1258 00:45:47,810 --> 00:45:48,469 you for your time. 1259 00:45:48,470 --> 00:45:50,509 It was interesting because I think I have 1260 00:45:50,510 --> 00:45:52,939 a question. Is it possible to make 1261 00:45:52,940 --> 00:45:54,289 errors a little better? 1262 00:45:54,290 --> 00:45:56,929 I mean, are to detect 1263 00:45:56,930 --> 00:45:58,999 some example type 1264 00:45:59,000 --> 00:46:01,489 mismatch and write 1265 00:46:01,490 --> 00:46:04,969 that the file was not closed, 1266 00:46:04,970 --> 00:46:06,619 that case? That's possible. 1267 00:46:06,620 --> 00:46:08,899 So someone's working on this 1268 00:46:08,900 --> 00:46:11,149 thing called our reflection, and it 1269 00:46:11,150 --> 00:46:13,399 gives you a type structure, a data 1270 00:46:13,400 --> 00:46:15,319 structure that represents this error. 1271 00:46:15,320 --> 00:46:16,699 And you can write an interest program 1272 00:46:16,700 --> 00:46:18,799 that interprets that error message 1273 00:46:18,800 --> 00:46:20,209 and gives you something that a human can 1274 00:46:20,210 --> 00:46:21,960 actually read this. 1275 00:46:23,000 --> 00:46:24,319 So this is one of the things why the 1276 00:46:24,320 --> 00:46:25,669 penalties are research. 1277 00:46:25,670 --> 00:46:27,439 We don't really know how to handle this 1278 00:46:27,440 --> 00:46:29,599 stuff. It's it's very hard 1279 00:46:29,600 --> 00:46:31,849 to write big applications in address 1280 00:46:31,850 --> 00:46:32,999 at the moment. 1281 00:46:33,000 --> 00:46:34,599 OK, over to Mike. 1282 00:46:34,600 --> 00:46:37,009 Yeah. Hey, how is it 1283 00:46:37,010 --> 00:46:38,059 implemented? 1284 00:46:38,060 --> 00:46:40,629 Is it running in a VM is itself hosted? 1285 00:46:40,630 --> 00:46:42,709 It's it's not self hosted at the 1286 00:46:42,710 --> 00:46:43,759 moment. 1287 00:46:43,760 --> 00:46:46,429 It's it's really in Haskell. 1288 00:46:46,430 --> 00:46:48,409 So if yes. 1289 00:46:48,410 --> 00:46:49,519 I love Haskell. 1290 00:46:49,520 --> 00:46:51,079 So it's a great language. 1291 00:46:51,080 --> 00:46:53,269 So we are planning to 1292 00:46:53,270 --> 00:46:55,639 rewrite it maybe at some point, 1293 00:46:56,660 --> 00:46:58,669 but there are not a lot of things in 1294 00:46:58,670 --> 00:46:59,659 place that we need. 1295 00:46:59,660 --> 00:47:00,949 So we've got this part of the library 1296 00:47:00,950 --> 00:47:02,839 called Licia, which is a pun on Parsec 1297 00:47:02,840 --> 00:47:03,840 from Haskell. 1298 00:47:05,750 --> 00:47:08,059 And this this is what I'm using 1299 00:47:08,060 --> 00:47:09,060 in this in this 1300 00:47:10,130 --> 00:47:11,509 in this case, we Pavo. 1301 00:47:11,510 --> 00:47:13,039 So we need stuff like that. 1302 00:47:13,040 --> 00:47:15,229 We need when when you look at the at 1303 00:47:15,230 --> 00:47:17,209 the it was interpretor or the compiler, 1304 00:47:17,210 --> 00:47:18,829 it has a lot of dependencies and we are 1305 00:47:18,830 --> 00:47:20,149 not nearly there. 1306 00:47:20,150 --> 00:47:22,429 So maybe at some point 1307 00:47:22,430 --> 00:47:24,589 we'll be self Holsted it's but it's not 1308 00:47:24,590 --> 00:47:26,599 a priority but so what is it. 1309 00:47:26,600 --> 00:47:27,920 So the compiler generates, 1310 00:47:29,240 --> 00:47:31,549 the compiler generates generates C 1311 00:47:31,550 --> 00:47:32,999 and puts an object. 1312 00:47:33,000 --> 00:47:35,209 OK, so it generates 1313 00:47:35,210 --> 00:47:36,769 JavaScript or whatever. 1314 00:47:36,770 --> 00:47:37,770 Yeah. 1315 00:47:39,280 --> 00:47:41,459 Like one, I 1316 00:47:41,460 --> 00:47:42,789 have two questions, actually. 1317 00:47:42,790 --> 00:47:44,949 OK, first one, do you 1318 00:47:44,950 --> 00:47:47,199 have any other any projects 1319 00:47:47,200 --> 00:47:49,599 that you know of that try to apply this 1320 00:47:49,600 --> 00:47:51,909 typing to imperative programing languages 1321 00:47:51,910 --> 00:47:53,409 as opposed to functional? 1322 00:47:53,410 --> 00:47:55,359 Excuse me, I didn't get there. 1323 00:47:55,360 --> 00:47:57,609 Are there any are 1324 00:47:57,610 --> 00:47:59,709 there any experiments trying to project 1325 00:47:59,710 --> 00:48:01,989 dependent typing to imperative programing 1326 00:48:01,990 --> 00:48:02,990 languages? 1327 00:48:03,970 --> 00:48:06,099 I know of a project that's called Flow 1328 00:48:06,100 --> 00:48:08,539 that is run by Facebook. 1329 00:48:08,540 --> 00:48:10,389 It's something that does statically 1330 00:48:10,390 --> 00:48:12,459 checking on on JavaScript. 1331 00:48:12,460 --> 00:48:14,919 And I've I've seen some of the ideas. 1332 00:48:14,920 --> 00:48:16,959 So this branches, if then else branches, 1333 00:48:16,960 --> 00:48:19,749 it knows in which 1334 00:48:19,750 --> 00:48:20,919 part of the branch it is. 1335 00:48:20,920 --> 00:48:22,869 And I don't know if it really qualifies 1336 00:48:22,870 --> 00:48:23,889 as being dependably typed. 1337 00:48:23,890 --> 00:48:24,429 I don't think so. 1338 00:48:24,430 --> 00:48:26,589 But there is a 1339 00:48:26,590 --> 00:48:28,689 there is a project that tries 1340 00:48:28,690 --> 00:48:30,279 to bring dependent types to JavaScript as 1341 00:48:30,280 --> 00:48:31,269 well. 1342 00:48:31,270 --> 00:48:32,270 Um, 1343 00:48:33,640 --> 00:48:35,859 Schola actually has dependent types. 1344 00:48:35,860 --> 00:48:37,809 It's it's pretty much the first 1345 00:48:37,810 --> 00:48:39,489 commercial programing language that 1346 00:48:39,490 --> 00:48:41,109 offers dependent types, even though not 1347 00:48:41,110 --> 00:48:42,639 full dependent types like we have an 1348 00:48:42,640 --> 00:48:45,039 address, but something 1349 00:48:45,040 --> 00:48:47,629 that is pretty powerful. 1350 00:48:47,630 --> 00:48:49,419 OK, next question. 1351 00:48:49,420 --> 00:48:51,489 The example of the trees where you 1352 00:48:51,490 --> 00:48:53,649 have this tree shaped type, how was that 1353 00:48:53,650 --> 00:48:54,649 actually implemented? 1354 00:48:54,650 --> 00:48:57,009 Do you do you have for every tree shape 1355 00:48:57,010 --> 00:48:59,529 one runtime object? 1356 00:48:59,530 --> 00:49:01,739 If you construct a new tree, you have to 1357 00:49:01,740 --> 00:49:03,849 do this. Every tree node construct 1358 00:49:03,850 --> 00:49:04,809 a new country. 1359 00:49:04,810 --> 00:49:06,519 You don't need a you don't need these 1360 00:49:06,520 --> 00:49:08,059 tree shapes at runtime. 1361 00:49:08,060 --> 00:49:09,639 They can get raised. 1362 00:49:09,640 --> 00:49:12,099 So you don't need to store your indices 1363 00:49:12,100 --> 00:49:13,449 so you don't have to carry around the 1364 00:49:13,450 --> 00:49:15,159 length of the vector as well. 1365 00:49:15,160 --> 00:49:16,160 So it just 1366 00:49:17,470 --> 00:49:19,449 isn't that isn't that isn't that needed 1367 00:49:19,450 --> 00:49:20,679 for the paper on that? 1368 00:49:20,680 --> 00:49:22,269 Bye bye, everyone. Brady that that's 1369 00:49:22,270 --> 00:49:24,549 called are how 1370 00:49:24,550 --> 00:49:26,379 is it called like of something like 1371 00:49:26,380 --> 00:49:27,729 adductor families don't need to carry 1372 00:49:27,730 --> 00:49:28,989 their indices or something like that. 1373 00:49:28,990 --> 00:49:31,149 I don't know if it's something like that. 1374 00:49:31,150 --> 00:49:33,009 You can't erase them. You don't need to. 1375 00:49:33,010 --> 00:49:35,079 Sometimes you carry them around when you 1376 00:49:35,080 --> 00:49:37,269 want to inspect them a runtime, but you 1377 00:49:37,270 --> 00:49:38,289 don't need them, General. 1378 00:49:40,350 --> 00:49:41,639 OK, over to Mike three, 1379 00:49:42,660 --> 00:49:45,119 quick question, is it as lazy as Haskell 1380 00:49:45,120 --> 00:49:47,399 now, so we've got 1381 00:49:47,400 --> 00:49:49,809 a strict construct, a lazy constructor. 1382 00:49:49,810 --> 00:49:51,599 You can have you can put laziness, 1383 00:49:51,600 --> 00:49:53,759 annotations and but 1384 00:49:53,760 --> 00:49:55,229 it's a strict language. 1385 00:49:55,230 --> 00:49:57,479 So this is this is geared toward system 1386 00:49:57,480 --> 00:49:59,279 programing. And Edwin wanted to have 1387 00:49:59,280 --> 00:50:01,379 something that that is actually strict 1388 00:50:01,380 --> 00:50:03,989 so you can reason about space 1389 00:50:03,990 --> 00:50:05,369 and stuff like that. 1390 00:50:05,370 --> 00:50:07,019 Easier, Mike, to 1391 00:50:08,460 --> 00:50:10,709 just the question about these types and 1392 00:50:10,710 --> 00:50:13,019 proofs that seem to have 1393 00:50:13,020 --> 00:50:14,129 I'm intrigued. 1394 00:50:14,130 --> 00:50:16,199 Does this do any propagation of 1395 00:50:16,200 --> 00:50:18,449 propagation to get the things 1396 00:50:18,450 --> 00:50:20,579 that you see there when it comes up with 1397 00:50:20,580 --> 00:50:23,009 a redefinitions, et cetera, or 1398 00:50:23,010 --> 00:50:23,939 do conflicts? 1399 00:50:23,940 --> 00:50:25,679 In other words, does it do an empty, 1400 00:50:25,680 --> 00:50:27,749 complete search and 1401 00:50:27,750 --> 00:50:29,699 aborts eventually when it's sort of like, 1402 00:50:29,700 --> 00:50:31,439 oh, well, I'll be searching for half an 1403 00:50:31,440 --> 00:50:32,639 hour and, you know, I'm not going to come 1404 00:50:32,640 --> 00:50:33,929 up with this definition anymore? 1405 00:50:33,930 --> 00:50:36,209 Or do you only do propagation 1406 00:50:36,210 --> 00:50:38,279 of facts like IBM or 1407 00:50:38,280 --> 00:50:40,739 the or the current compilers, let's 1408 00:50:40,740 --> 00:50:41,369 put it that way. 1409 00:50:41,370 --> 00:50:42,569 So I think that's a question that 1410 00:50:42,570 --> 00:50:44,219 probably Hadwin should answer. 1411 00:50:44,220 --> 00:50:46,409 I don't, I don't think I know the answer 1412 00:50:46,410 --> 00:50:47,719 to this. I'm sorry. 1413 00:50:47,720 --> 00:50:48,719 Yeah. 1414 00:50:48,720 --> 00:50:50,849 OK, like one. 1415 00:50:50,850 --> 00:50:51,989 Yes I have two questions. 1416 00:50:51,990 --> 00:50:54,629 Also the first one is 1417 00:50:54,630 --> 00:50:56,979 you showed some first order logic, 1418 00:50:56,980 --> 00:50:57,980 existential 1419 00:50:59,040 --> 00:51:00,869 and universal quantifiers. 1420 00:51:00,870 --> 00:51:03,089 Can you do also second order logic. 1421 00:51:03,090 --> 00:51:05,639 So quantum person sets or 1422 00:51:05,640 --> 00:51:07,409 or is that beyond the scope of the 1423 00:51:07,410 --> 00:51:08,410 language? 1424 00:51:08,860 --> 00:51:10,409 I didn't get that as well. 1425 00:51:10,410 --> 00:51:12,809 Sorry. So can you do second order logic 1426 00:51:12,810 --> 00:51:14,639 also or is it just first order? 1427 00:51:14,640 --> 00:51:16,109 Uh, also modal logic. 1428 00:51:16,110 --> 00:51:18,449 Is that in temporal modal logic or. 1429 00:51:19,590 --> 00:51:21,209 Oh, that's a good question. 1430 00:51:21,210 --> 00:51:23,429 I don't know if I really 1431 00:51:23,430 --> 00:51:24,819 need to try. 1432 00:51:24,820 --> 00:51:27,239 But also the second second question is, 1433 00:51:27,240 --> 00:51:29,429 um, so you 1434 00:51:29,430 --> 00:51:32,009 show this V example and 1435 00:51:32,010 --> 00:51:34,319 it seemed like do you actually like 1436 00:51:34,320 --> 00:51:36,449 to have the impetuses 1437 00:51:36,450 --> 00:51:38,519 be available for, like, 1438 00:51:38,520 --> 00:51:40,139 compiling? Yeah. 1439 00:51:40,140 --> 00:51:42,239 So, yeah, you can you 1440 00:51:42,240 --> 00:51:44,729 can use this in a like 1441 00:51:44,730 --> 00:51:47,729 another nice example will be like 1442 00:51:47,730 --> 00:51:50,399 table four for database 1443 00:51:50,400 --> 00:51:52,619 so you can call the database, 1444 00:51:52,620 --> 00:51:54,959 get the schema and types there. 1445 00:51:54,960 --> 00:51:57,059 So this is obviously it's just an 1446 00:51:57,060 --> 00:51:59,069 example. It's not really something that 1447 00:51:59,070 --> 00:52:01,499 is super useful, but I think it's 1448 00:52:01,500 --> 00:52:03,599 it's a neat example to to just demo a lot 1449 00:52:03,600 --> 00:52:05,819 of the stuff that what happens if it's 1450 00:52:05,820 --> 00:52:07,889 if if you feed it with a different 1451 00:52:07,890 --> 00:52:10,109 SISMI and then then you need 1452 00:52:10,110 --> 00:52:11,849 to. So you need to compile that once 1453 00:52:11,850 --> 00:52:13,919 again. Yeah. This is so it can't change 1454 00:52:13,920 --> 00:52:15,569 the program magically. 1455 00:52:15,570 --> 00:52:17,649 Just it's it's come out 1456 00:52:17,650 --> 00:52:19,919 and say you 1457 00:52:19,920 --> 00:52:23,279 need to actually check the input somehow 1458 00:52:23,280 --> 00:52:24,659 if you're running it, if the schema 1459 00:52:24,660 --> 00:52:26,849 changes you need to change a to 1460 00:52:26,850 --> 00:52:27,850 recompile. Yeah. 1461 00:52:29,370 --> 00:52:30,719 Signal and you'll do we have any 1462 00:52:30,720 --> 00:52:32,779 questions from IOC and stuff. 1463 00:52:32,780 --> 00:52:34,039 No. 1464 00:52:34,040 --> 00:52:35,040 OK, 1465 00:52:36,570 --> 00:52:36,839 Mike. 1466 00:52:36,840 --> 00:52:37,769 Sorry. Yeah. 1467 00:52:37,770 --> 00:52:40,119 So in that example if the file handles 1468 00:52:40,120 --> 00:52:41,489 that's the implication of that, that you 1469 00:52:41,490 --> 00:52:43,859 could not with a given types, 1470 00:52:43,860 --> 00:52:45,629 write a program but has to difficult 1471 00:52:45,630 --> 00:52:47,339 logic governing whether the handler was 1472 00:52:47,340 --> 00:52:49,949 in fact closed or 1473 00:52:49,950 --> 00:52:51,929 is it that compilation might in fact not 1474 00:52:51,930 --> 00:52:53,459 terminate? 1475 00:52:53,460 --> 00:52:54,460 Um. 1476 00:52:55,500 --> 00:52:57,269 Good question. Oh no, it's not it's not 1477 00:52:57,270 --> 00:52:59,639 really that. So you just you're 1478 00:52:59,640 --> 00:53:01,919 the type system that forces you to handle 1479 00:53:01,920 --> 00:53:04,019 these to tackle 1480 00:53:04,020 --> 00:53:06,329 these two cases. So you're not actually 1481 00:53:06,330 --> 00:53:08,339 compiling the file handle doesn't get 1482 00:53:08,340 --> 00:53:09,599 open during compilation. 1483 00:53:09,600 --> 00:53:11,429 So that's not what I mean. 1484 00:53:11,430 --> 00:53:14,309 OK, I mean, so 1485 00:53:14,310 --> 00:53:16,379 what is the I mean, basically, 1486 00:53:16,380 --> 00:53:18,659 presumably have a certain logic 1487 00:53:18,660 --> 00:53:20,639 which is captured by this type system, 1488 00:53:20,640 --> 00:53:22,709 which it might or might not 1489 00:53:22,710 --> 00:53:24,959 be desirable. And if it's the citable, it 1490 00:53:24,960 --> 00:53:26,549 probably means that you cannot prove 1491 00:53:26,550 --> 00:53:28,059 things that are particularly complicated. 1492 00:53:28,060 --> 00:53:30,989 But programs cannot prove 1493 00:53:30,990 --> 00:53:32,099 the termination of particularly 1494 00:53:32,100 --> 00:53:34,289 complicated programs they 1495 00:53:34,290 --> 00:53:36,839 can say of type system to citable. 1496 00:53:36,840 --> 00:53:38,999 That's what I'm ultimately asking, 1497 00:53:39,000 --> 00:53:41,819 is the types of undecidable are I? 1498 00:53:41,820 --> 00:53:44,099 That's I think that should be 1499 00:53:44,100 --> 00:53:45,100 the. 1500 00:53:46,960 --> 00:53:49,199 Dependent, dependent type checking 1501 00:53:49,200 --> 00:53:51,389 is I don't I think there was a paper that 1502 00:53:51,390 --> 00:53:53,759 says it's not desirable, but I'm 1503 00:53:53,760 --> 00:53:54,809 very thin ice here. 1504 00:53:54,810 --> 00:53:57,089 This is so so you're asking theoretical 1505 00:53:57,090 --> 00:53:59,939 questions. I'm just some compiler 1506 00:53:59,940 --> 00:54:01,509 wannabe hacker. 1507 00:54:01,510 --> 00:54:03,959 Just I'm not too sure. 1508 00:54:03,960 --> 00:54:06,519 You know, this is perfectly fine. 1509 00:54:06,520 --> 00:54:07,520 Yeah. 1510 00:54:08,220 --> 00:54:09,879 Mike, please. 1511 00:54:09,880 --> 00:54:10,880 If you 1512 00:54:13,050 --> 00:54:14,959 if you have a question, Gary's come to 1513 00:54:14,960 --> 00:54:16,139 Mike. 1514 00:54:16,140 --> 00:54:18,329 So he's he's 1515 00:54:18,330 --> 00:54:19,599 got the answer to your question, I think, 1516 00:54:19,600 --> 00:54:20,949 sir, that. 1517 00:54:26,760 --> 00:54:28,499 So we can take this country. 1518 00:54:28,500 --> 00:54:30,869 Can you go to a microphone, please? 1519 00:54:30,870 --> 00:54:32,210 So how many recordings? 1520 00:54:33,420 --> 00:54:36,089 I have a question regarding the example 1521 00:54:36,090 --> 00:54:38,279 for the file handling 1522 00:54:38,280 --> 00:54:40,469 the closing of the file 1523 00:54:40,470 --> 00:54:43,319 cannulas where there is an 1524 00:54:43,320 --> 00:54:45,419 error if the file is 1525 00:54:45,420 --> 00:54:46,349 not closed. 1526 00:54:46,350 --> 00:54:48,509 Yeah. And is it possible 1527 00:54:48,510 --> 00:54:51,719 to generate the closed, closed 1528 00:54:51,720 --> 00:54:53,339 statement automatically? 1529 00:54:53,340 --> 00:54:55,739 So to satisfy that the 1530 00:54:55,740 --> 00:54:57,959 file is closed at the end, that's 1531 00:54:57,960 --> 00:54:59,129 automatically closing. 1532 00:54:59,130 --> 00:55:00,509 That's yes. 1533 00:55:00,510 --> 00:55:01,919 That's a good question. I don't know 1534 00:55:01,920 --> 00:55:02,189 that. 1535 00:55:02,190 --> 00:55:04,709 But if it might be 1536 00:55:04,710 --> 00:55:07,019 possible, because the same 1537 00:55:07,020 --> 00:55:09,329 same thing can be applied to the memory 1538 00:55:09,330 --> 00:55:11,129 management or research resource 1539 00:55:11,130 --> 00:55:12,150 management in general. 1540 00:55:13,760 --> 00:55:15,649 I don't I don't know, I haven't tried 1541 00:55:15,650 --> 00:55:17,380 that could be possible. 1542 00:55:19,930 --> 00:55:22,189 Probably thinks so, 1543 00:55:22,190 --> 00:55:24,809 let's find out, maybe stack on it. 1544 00:55:24,810 --> 00:55:26,800 OK, last question, Mike, three. 1545 00:55:29,570 --> 00:55:31,819 Do if this language only a 1546 00:55:31,820 --> 00:55:33,919 proof of concept or do you plan 1547 00:55:33,920 --> 00:55:35,749 to support it a long time? 1548 00:55:35,750 --> 00:55:37,270 And what are your plans to 1549 00:55:38,360 --> 00:55:39,800 implement next? 1550 00:55:41,210 --> 00:55:42,949 This is once again a question that should 1551 00:55:42,950 --> 00:55:45,169 be asked to anyone, but we talked 1552 00:55:45,170 --> 00:55:47,059 about this quite a lot. 1553 00:55:47,060 --> 00:55:48,709 This is an experiment. 1554 00:55:48,710 --> 00:55:50,659 There are a lot of different approaches 1555 00:55:50,660 --> 00:55:51,569 to dependent types. 1556 00:55:51,570 --> 00:55:52,639 There are a lot of different kinds of 1557 00:55:52,640 --> 00:55:54,709 type, like intentional type, 1558 00:55:54,710 --> 00:55:56,179 extensional type theory, observational 1559 00:55:56,180 --> 00:55:57,709 type theory there. 1560 00:55:57,710 --> 00:55:59,869 People try to come up 1561 00:55:59,870 --> 00:56:01,519 with all sorts of different approaches 1562 00:56:01,520 --> 00:56:04,069 there, and it was pretty 1563 00:56:04,070 --> 00:56:05,539 conservative in its approach. 1564 00:56:05,540 --> 00:56:07,759 So we just it's just one 1565 00:56:07,760 --> 00:56:10,569 way maybe it will turn into 1566 00:56:10,570 --> 00:56:12,169 a programing language that can use in 1567 00:56:12,170 --> 00:56:13,999 production, I don't know, ten years. 1568 00:56:14,000 --> 00:56:15,920 I don't know, maybe never. 1569 00:56:16,940 --> 00:56:19,039 So this is so currently this is 1570 00:56:19,040 --> 00:56:21,799 just a fun project to to find out 1571 00:56:21,800 --> 00:56:24,289 where it's where we're going with that. 1572 00:56:24,290 --> 00:56:25,290 We can go with that. 1573 00:56:26,570 --> 00:56:27,570 Yeah, sure. 1574 00:56:29,250 --> 00:56:30,779 All the housekeeping now, if you're 1575 00:56:30,780 --> 00:56:34,109 leaving, take anything with you and 1576 00:56:34,110 --> 00:56:35,849 a round of applause for Rachel. 1577 00:56:37,720 --> 00:56:38,949 Thanks for your attention.