So, hello everyone. I'm Mark Ferrell. I'm a second year student at the University of Waterloo up in Waterloo, Ontario, Canada. And today I'm going to be talking about Typed Racket. Typed Racket adds an optional static type system to Racket, allowing you to ensure that some aspects of your program's behavior are correct before they run. Now, Typed Racket's designed to accommodate the style in which you would program an untyped racket and use your untyped racket programs in Typed Racket with minimal modification. Typed Racket achieves this by equipping its type system with a number of features, notably occurrence typing, which allows you to derive types from predicate tests inside the body for definition. So, untyped racket programmers would write functions where you might say, if X your input is a string, then do this, or if it's a number, then do that. That's just what they do. So occurrence typing accommodates the style of programming. That leads me to my next point. Typed Racket also has untagged union types, so you can have the union of a string or a number, and the habitants of that type could either be string or numbers. If you had a function that, if X is a string, does one thing, and if a number does another thing, then the type of that definition would be, the function would reduce the union of a string or a number. Typed Racket also has subtyping, having any as the top type, nothing as the bottom type, and for instance, real as a subtype of number. And lastly, it makes all values types, because what you might do sometimes is say that if X is a valid input to your function, then do something and produce some value, or else produce exactly the symbol error, which would be a value, so they make all values types. We'll have a look at these particular features that help you, that make it, so that you can use your untyped racket programs in Typed Racket with minimum modification later on this workshop. But first, let's get you using Typed Racket, type-and-adding examples of previously untyped racket code, perhaps looking at some more familiar features of Typed Racket's type system. As the show of hands, how many of you have already downloaded and installed Racket and Dr. Racket? So you're all good. And Racket 6.1.1, the latest one on the website? Okay. And how many of you have not? Sorry. Okay. Now would be a good time to do so. It might take you a couple minutes. We'll just go over some basic examples. For instance, type-anotating the definition of, say, a person's full name. Here, John Smith. So we want John Smith to be a string, and string is a basic type-and-type racket, so you just type open parentheses. So to type-anotate this definition of, we know that John Smith is a string, but we want to make sure that John Smith is a string before our program runs. So we just type-anotate this definition by saying that full name is a string. It's a basic type-and-type racket. And you change the language from racket to typed racket and hit run. And you just... Run is in Dr. Racket's button up at the top right corner. And so if you type full name at the interpreter here, you could see that it's a string. Okay. So suppose this person's age is 28, like an example. Any thoughts on how you might type-anotate that? First of all, how many of you are familiar with racket? Not typed racket, but just racket. Okay. Any thoughts on how you might type-anotate this definition based on what you know about types and... I hate saying un-typed racket, dynamically typed racket, yeah. Based on what you know about, like, racket's numeric types. It does its... So yeah, you could say that age is a number, and that would be correct. I was expecting that some of you might say that age is an integer. More precisely, you could say that age is a positive integer. There's, I believe, on the racket manuals, there's a diagram explaining racket's numeric type-herarchy. I'm not saying it's nice. I'm just saying that, like, you pay attention to that. Like, you could be most precisely saying that age is a positive integer rather than integer or number. And it uses subtyping. So, like, number is a subtype. I mean, integer is a subtype of number and positive integer is a subtype of integer. All right. So, okay, now we're going to look at some function definitions in typed racket. Positive, yeah. You could say that age is a positive integer. And that would probably, that would be most precise with, in racket's numeric types, yeah. How many of you are good at, or have gotten that far? Okay. So, sir, in the console, is there a way that you... Yeah, there's, you could print type age and just get its type. And if you have a type, which we'll see later on, like, if you say, you could say, what's the type of number? It'll tell you that number is exactly the union of, like, all of these subtypes. Okay. So, let's type a GC... Let's look at how we might type functions in typed racket. Suppose we have a GCD function that computes the greatest common divisor of A and B. We can implement this function using modulo. Now, this function works for all integer inputs. Oh, sorry. Question? The square brackets, that's just a convention. Everything's just, yeah, all you have is S expressions in racket. But you don't need that. It does it for you in doctor, in doctor racket because that's a convention. But if you just did this in a text editor, you could just use the, like, round parentheses and that would be fine. Yeah. Though don't do that. Use the square braces in con because that's just the convention, yeah. Now, you could type annotate this function by just saying it's a function type that takes an integer and integer and gives you an integer because it works for all integers including negative integers. For instance, the GCD of negative three and four is one and that would be fine. But suppose we... Let's call that GCD one. You can also implement GCD only using subtraction. And if you implement GCD with only subtraction, that's a problem because if you give this function negative integers as inputs, it won't terminate. You couldn't take, like, the GCD of negative three and four in this case. Oh, my bad. Sorry, I think I have an extra set of parentheses here, yeah? Does that... Are you okay now? Yeah. Okay. So when should you use a bracket and what is the convention? Just with conned, notably conned, yeah. Conned, match. Change clause and conned. You should use the square brackets. Note that Dr. Rector should be doing that for you, yeah? You shouldn't be able to type... I don't think it'll... It'll... I think it did it... Perhaps not. Perhaps it doesn't do it for you, but you should use the square parentheses there. You don't have to though, like, don't worry about it, I guess, yeah? Okay, so this GCD function won't terminate if you give it negative integers unlike the previous GCD function that we looked at that was implemented using modulo. So you want to enforce the constraint that you can only give it non-negative integers as input. Oh, that's just... Like, there's just two implementations of GCD. I just took... You can implement GCD using... Okay. It's just...  Oh, sorry, that should be else GCD be modulo AB, yeah? Yeah. But yeah, if you don't have an else clause and you don't... And you reach the end of your clauses and you don't have a clause to handle a particular case of input, then it will throw an error at runtime. Anyway, you'd want to enforce the constraint here that GCD takes non-negative integers as input. And in untyped bracket, you could use contracts to guard the function at runtime. So if you give it non-negative integers as input, it would throw an error. Yeah. So in untyped bracket, you can guard functions by saying, like, specifying what's valid input. And if you don't give it a valid input, it will throw an error at runtime. You can diagnose where in your program, you're not meeting specification, but you can only diagnose where it's happening at runtime. You can only guard functions themselves. It's not, like, transitive, like, type checking, yeah? So you could say that this function has to take an exact non-negative integer, an exact non-negative integer, and give you an exact non-negative integer. Yeah. So, like, actually, these should be predicates. So you'd say it would test that A is an exact non-negative integer, an exact non-negative integer, and B is an exact non-negative integer, and then it has to give you an exact non-negative integer. So, yeah. So, for example, like, you do a lot of, like I said, a dispatch by predicate testing in Racket, and so, for example, when you define your own structs in that type bracket, say, a position, like, an xy coordinate, it would, and you say, like, struct, pause in xy, and you create that, define that struct, and it also creates a predicate pause in the test that something's of the type pause in at runtime. So, exact non-negative integer is a numeric type of type bracket. For example, like, 3.0 is not an exact non-negative integer. However, like, it would be a non-negative integer. That's how Racket treats types. Yeah. Like, I personally feel as though type Racket's numeric type system is not, like, I think we've gotten further than that in programming, like, but that's the way it works. Yeah. So, you can't take, like, the GCD of negative three or four. You get a contract error. However, if we try to enforce the same constraint in type Racket and enforce that constraint before a program runs, we run into the issue of having to actually cast the result of subtraction in this definition even if we think it's correct, even if we know our program's correct, we still have to cast. Yeah. Of course, types. So, we want to say that GCD takes an exact non-negative integer. Exact non-negative integer. Exact non-negative integer. You can't say that even if we know this is correct, you can't say that when we subtract negative B from A in these two cases that it's an exact non-negative integer, even though if we know that if we give, that it will be for all exact non-negative integers that we give to this function. So, we have to cast to an exact non-negative integer. When you say colon, the origin of colon is the first thing that is in the list. That's the type annotation. So, you say that the func, like, this is, like, type Racket, like, adds a type system to Racket. So, the idea is that you might, for instance, like, you could do this in comments, like, on type Racket programmers kind of comment types like this with this convention, like, colon GCD, like, function type exact non-negative integer, exact non-negative integer. But in type Racket, it's, like, you can uncomment that and then it will type check. Yeah? Yeah. The comment's been converted to something mythical. Yeah. Jack's for you. Yeah. So, it's kind of like the syntax here for type annotations. It's kind of like this convention that people have been doing in comments for quite some time, at least in my first year course work. Like, we would actually make us, like, comment type annotations in this convention.  Now we could start uncomment. Like, these are types. Let's introduce you to the idea of types. Let's uncomment your comments and then type check. Yeah? Yeah. So, like, the contract syntax is a little bit different, though. You're saying that, yeah, it's a function, a function, like, this arrow means it's a function type that takes the type exact non-negative integer A. The exact non-negative integer A will produce an exact non-negative integer A. Yeah, it's type bracket syntax for a function type, yeah? And just another question. So, that sort of syntax is standard in Haskell because everything is curried by default. Yeah. Is that the case in Racket? Not really. I don't, it's not curried. It's just, you can curry functions in Racket, but I don't think that that's the idea. It's just. But they just put it that way. They just put, this is just the function type syntax. Yeah, it's not curried by default. Yeah? I'm sorry, since we mentioned comments, what is the comment character for? Uh, colon colon. Yeah. Okay. So, you have to cast this to exact non-negative integers. Yeah, it's a non-sevcast. We know it's correct. We don't want, we don't want to say that we can, we don't want to give this, be able to give this function negative integers in because it won't terminate. So, we, this is what, I think this is the best we can do to say that GCD takes an exact non-negative integer and exact non-negative integer gives you exact non-negative integer. And you can't, you can't use contracts with types in type Racket for one thing, like meaning you can enforce some constraints of compile time and enforce some constraints at runtime. You can't do that. For one thing, I mean as, as, as you mentioned there, like the syntax is similar for like how you'd say, how do you'd express function contracts and how you'd express function types. So we can't, there's already kind of, there might be some way to, in principle, use contracts with types to enforce some constraints of compile time and sometimes at run, some at runtime. However, we can't do that right now just, just for, we just can't do that right now in Racket. Yeah, that's true. Yeah, you can't use contracts. These, those are two different files. I actually did contracts first here and then changed it to type Racket and then showed you how, this is how you do it in contracts and then this is how we type it. Yeah. Go from contracts to static type. It was originally Racket when I, when I showed the contract in like the contract area here. You could jump it back and forth like before. It's really, it's really hard to try to follow along and do what you're doing in Racket. You're going very quickly and assuming a lot of knowledge. You're in Racket, you probably say now I'm in Racket, now I'm in type Racket because I'm trying to, you know, type this in. Okay. Do you want me to go back? No, no. Now I know what's going on. Okay. Here's just a general conceptual thing about, about the application. I'm going to make sure I've got this right. Everything you type up in the top is, if it's a file and if we hit run, it's going to process everything that's in the upper section completely. It's not like it's evaluating line by line. It just interpret processes everything up there and, and is that right? Yeah. Okay. Yeah. So we have to cast here and then we can't, for instance, give it a negative integer as input because that's, it, it, negative three doesn't have the type of exact on negative integer. So we guard from, from being able to do that. So if we use programs that, that use GCD, it won't type check and we won't be able to run our program if you try to take the GCD if some negative number anywhere. Yeah. Sorry. So if you, you, you won't be able to run your program if you try to take the GCD if a negative integer anywhere in there. Um, I'm not sure. I think you did. So it'll, yeah, there'll be a run, a contractor at runtime. Yeah. Yeah. So we can't, we can't guard against that before a program runs then in that case. But I believe this is the best we could do if we want to try to enforce the constraint that our GCD functionally take, can't take non-negative integers as input. Cast is unbound. Are you in typed racket? Poundlang type. Oh yeah. You have to change your language to type bracket. Yeah. Yeah. So like the idea is like we're, we're type annotating, we're going from bracket to type bracket and I'm just showing you how you type annotate previously on type bracket code to enforce constraints before your program runs. Okay. So as an exercise, how would you type annotate function that computes the NSFibonacci number? I'll give you like two minutes to do that. How many of you have fully, oh there's the type bracket guide. So just like look at what we just do with the GCD function. Like the GCD function takes two integers, two exact non-negative integers as input and gives you an exact non-negative as output. Just, just using what we did, did there and what we did with age in the previous example, like exploring basic types, how much you type annotate this Fibonacci function. Like this, are you, like if you, are you all familiar with the Fibonacci sequence? Like this would take like one and give you one, two and give you two and whatever the next element in the Fibonacci sequence is. Yeah. Are those of you who haven't downloaded and installed Rack of Before this workshop, are you good now or you're good? I'm on edgerome, so I'm able to use the same login that I use at other universities. I guess throughout North America, yeah. Yeah. As a show of hands, how many of you know, think you know how to type annotate this function or have successfully done it? You're good. Okay. Do you want to give an answer to a natural? That type check is in the Fib function? Yeah. Yeah. That's the idea I was going for. Like you can give the Fibonacci function negative integers as input and it will terminate, but we want the Fibonacci sequence to start at one as input, so like you should do something similar. I'd actually say that this function's type signature should be, should a Fib should take a positive integer and give you a positive integer, but you have to cast. You could, that's a design decision you'd have to make like since Fib will terminate for negative numbers as input, you could just say that it takes an integer and gives you an integer. I'm saying like you could still be more precise with, by saying it's a positive integer because you want that to start at one, but you have to cast and like with GCD you have to cast and I think that's the best we can do a type record right now. What you had and it gets an error saying there's a type mismatch even though there's no types mentioned at all. Yeah. I think I made a mistake where I didn't say Fib twice. Like I tried to apply Fib to two arguments rather than doing plus Fib of n minus one. Yeah. I see. Okay. Yeah. Apologize. Yeah. We'll get to that though, but that non in this example, I don't think it's relevant for this example. That's sort of where I'm going so that's good. Yeah. Yeah. You could. Yeah. I'm actually going to show you something cool how we might add like Aida inspired range types to type brackets saying that here's my type for a person's age. It has to be between 60 and 80. We're going to like when we look at record types with name, age, faculty, and term and we only want their ID to be between certain positive integers and their age to be between say 16 and 80 for the example. And let me get to that. Yeah. Okay. So are you all good here? Okay. So now we're going to look at record types and type bracket. Record types are like product types where each field has a name and type bracket they're called structs. You could have structs and non-type bracket as well but they only know about them at, Racket only knows about them at runtime. So let's begin by, as I mentioned, like looking at this structure for this record type for a hypothetical student. So in non-type bracket you could say that this student has a field for their age, name, I mean their ID, name, age, faculty, and term and we're back and just racking. And I want to show you how we're creating this record type for a student. I suppose but I'm not sure the theme for my workshop is how we go from un-type bracket where it's difficult to enforce constraints. We certainly can't enforce any constraints about our, like we have some software specification. We can't enforce those constraints in our specification before our program runs. And I'm just showing how you'd go from un-type bracket where you can't enforce those constraints at least before your contracts but not that far. And how we add types to enforce those constraints before our program runs. So I'm not, yeah. I think ideally if this were in a classroom then the audience would best be somebody who took like one CS course that taught scheme and then were producing types in their second course or something like that. I'm not sure how else to teach types, yeah. So as an example here we could create record types in un-type bracket and we could create a student at runtime and say that their ID is an error for example that their name is 2, that their age is mark, that their faculty is nonsense, that their term is 6a, that they're in 6a which doesn't make sense if you're a graduate student and an undergrad and you only have 8 terms. So you can create these invalid students at runtime and un-type bracket and can't enforce those constraints that we talked about. However we switch over to typed bracket we can enforce the constraints that we'll start by enforce the constraints for faculty and term as I mentioned like you have untagged union types and all types are values and typed bracket those are features of a type system so what you can do is you can define a type for faculty for instance and say that faculty is the untagged union of the mathematics symbol science, engineering, arts or applied health sciences I'll break that up. Yes or no? So as I mentioned you can use a lot of previously un-typed bracket programs and typed bracket and it will try to infer types wherever it can. It equips its type system with the features that I mentioned to make it so that there's as little friction as possible when going from un-typed bracket to typed bracket. That's not necessarily good because if your design is flawed originally in un-typed bracket or if you have some, if it doesn't meet some specification that you set even though you believe it does just adding types that just compensate for that incorrect code doesn't do much but the idea is like to go to have little friction to be able to reuse the tools that people built in un-typed bracket when going to type bracket which is safer like which is hypothetically safer if you go from incorrect design incorrect your design with types though you since you can use un-typed bracket code often times in type bracket it will infer types about your un-typed bracket code which could be incorrect that's not necessarily good but I guess that's sort of the theme of gradual typing to add types gradually enforce constraints and cat shares and with little friction of and still being able to use your previously un-typed bracket code your un-typed code as much as possible and I noticed I think I noticed when you added changes over the typed bracket that struck it immediately popped up an error at the bottom saying that ID needed a type and I wasn't quite sure why that was you saw in other words before you did the faculty thing and you changed it from bracket to type bracket there was an error at the bottom complaining about ID saying that it didn't have a type so I wasn't clear on what the rules were when it would insist that you type it for structs you need since if you had an un-typed bracket module with student in it that's un-typed and you wanted to use it in a type bracket module that would be a case where you have to say what the types of each field are and you're struct there are many cases where you don't have to do that but there are some cases where you do and with like structs that would be a case where you do yeah type bracket generally it says if you have a struct then you have to type it tries to minimize friction if possible it just minimizes friction like there's still a case where you have to explicitly type annotate your previously un-typed bracket could so if we have this type for faculty and I mentioned we want to ensure that like our students term is valid as well in union defined type sorry it should be defined type yeah don't run it yet though because we haven't typed the struct yeah so I don't think it'll type check so we can like for instance when we do type we say that for instance that that their id will be our id type we want their name to be a string their age to be a valid age their faculty to be faculty to be a valid faculty and their term to be a valid term but like what we did here with faculty like we want we can enforce the constraint that their faculty is valid by saying it's only it's either health sciences nothing else is a valid faculty but as I mentioned how the only valid terms in an undergraduate's career might be 1A 1B 2A 2B 3A 3B 4A and 4B so thoughts on how you might create this type for term to enforce that constraint similar to how we did it with faculty yeah union of symbols yeah the union of symbols now the forcing like we already said the name is a string so we don't need anything there now enforcing the constraint that their ID and age is valid we want the age to be only between positive measures in the range 0 to 99 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 999 this, yeah. So, okay. So, I want to show you, yeah. So, like in ADAR, for instance, I believe you can have range types. You could define a type in ADAR, for example, saying type age is in the range 16 to 80, type ID is in the range 16 to 99,999,999. But in Racket we can, we can add that feature with macros, like effectively create range types like we do in ADAR. And so, what I want to do is show you how to do that. So, we can create macros and macro expansion takes place before type checking and type bracket. So, that's fine. So we define this syntax rule and we'll call it define range type. First, let's actually just create like what we want our range type for age to look like in ID. So, we want to be able to type define range type age 16 to 80, like the age is in the range 16 and 80. And we want ID to be in the range 0 to 99,999,999. And we define a syntax rule saying that where we say, we start by saying define range type and then some syntax object and then say match on the syntax object, pattern match on it. And in the case that the person says define range type, some type name, a lower bound on the range and an upper bound on the range, then we effectively what we do is we want to start by actually creating syntax that says define type age and actually print the syntax union 16 and then list out all the numbers 16, 17, 18, dot, dot, dot, 80. Close parentheses, close parentheses. Like we want to actually print that syntax before type checking occurs. Now, a range function isn't available when macro expansion occurs. It's like, I think there's different phases to how rocket programs are macro expanded type checked and what not before they run. And range isn't available at phase one. So, we have to actually create a range one. The left hand bracket. Is that? Oh my bad, I think I missed. No, wait, what's that? Yeah, I have to put, I'm not sure why it's aligning. Just give it, like maybe if we, I think maybe once I close all of my parentheses, that won't be an issue, yeah? So yeah, so syntax case lets you pattern match on the syntax object, which we want in this case to be, make it so you provide a type name, a lower bound and an upper bound. And then if you give it this valid syntax, then you can actually like, we want to be able to list, we want to be able to actually print the syntax define type age, like the actual type name that you provided, the actual like, and then the union, we want the type to be the union of all integers in the range from the lower bound to the upper bound and actually print it out and then give you that syntax object back and actually insert that into your program before type checking occurs, because we can expand macros before type checking in type bracket, yeah? If you're asking about actual mechanics about how the macro system works in type bracket and type bracket, that's a little bit more involved, but there's a manual, like for the sake of the example, please just like, fall along, yeah? Okay, and then after we have our let reckon, we have our range function, we want to use something called Kazai syntax that will allow us to print, actually compute a range and like, like list a range, like actually make a range, which is a list of integers and then take that list and just print out like 16, 17, 18, 19, 20, whatnot. If you're familiar with like string interpolation and whatnot in some programming languages, that's kind of how this works, but with syntax, yeah? So we want to actually, actually to print, define type or actual type name, we want it to actually write union and then we use unsyntax splicing. Yeah, there's, you can use, there are shorthand rules for like untax and syntax splicing and quasi, Kazai syntax, but I don't like using those, because I don't think it makes it as clear as to what's actually going on. Yeah, something, yeah, yeah. Oh, my bad. Can, sorry, could be, where's this? Yeah. Compar. Sure, I don't think we need to, oh, you mean I want a type that say is, it has to be less than three or greater than five, but not in between? Yeah, I'm not sure. I think like you could do some sort of comparison here before you untynt-syntax splice inside this macro, but we don't need to do that for any, yeah? I'm not sure. Do you mean to find operations of type like be able to add two range types or? I'm not sure. That's something that would be worth looking into, but I haven't thought about that, yeah? You could take the union of two range types and that would be fine. If you had two ranges, you could actually just union them and then it would be any values within that range. So, as I said, if one range is zero to three and the other is five to seven, yeah, you could just union those types and that would be fine. Yeah, it would be the union of those ranges, yeah. To union two range types? So, like, do you want to take the, like, define a type like foo and say it's the union of age and ID, for example, or could you be more, I'm just not following what? Okay, so, let's say that one age is less than that.  Yeah, I don't think you can like, you might be able to make like some sort of, sorry. Just let me run this program and I might need to fix that one sec, yeah? Can you see this? Do you want me to zoom out? Syntax data and syntax, that presumably interprets the AST, which is the lower bound in order to get you a value between a value and a range function? So, can you repeat that? Where you call in syntax data and syntax lower bound, that seems like that has to actually interpret the, I'm assuming that lower bound, as it's passed into our defined case, or as we obtain it from our defined case, is a chunk of syntax tree. Yeah, we originally get a syntax object, we have to, yeah, at some point we have to actually convert that back to values to compute, it's actually compute the range and create a list, which is the range, and then unsyntax plays like lists out the numbers in that range in syntax, yeah, rather than making it a list, like it unsyntax placing, we actually have to compute that list and then it takes the like list and just lists it out as syntax, like prints it, yeah. It turns it back to like a value, so we can actually compute the range before, yeah. I'm not sure I'm not familiar with common list. I know that Racket's macro system focuses on safety and making it sure that your macros are hygienic, and I don't know if eval is somehow unsafe in that sense, yeah. I think that's because, yeah, when we have a union type that's explicitly union of 0 to 999 million, 999,999, we run into that problem. I think you're going to run into that problem. Yeah, I think you can increase the memory limit, I just, yeah. I don't think you can like enforce constraints about constraints, your just program wouldn't like type check, it wouldn't like finish mac or expanding and it wouldn't type check if you like try to create it like an infinite type, yeah. Yeah, so that's the idea, like if we could have a contracts for this, these student and untyped Racket and we could define a predicate saying like valid ID and it has to be in this range and that would be easy, you just check at runtime, you wouldn't have any issues. I mean like it, you couldn't enforce a good straight before your program runs so your program could fail, like, but you know where it fails with contracts as opposed just passing around invalid students without contracts, but, and yeah, you wouldn't run into that issue, but in order to enforce a good straight for students that could pile time, like this is what, what I, what I believe you have to do, you have to create this, this range type, be able to define range types and specify the range and then let ages in this range, ideas in that range and then enforce that, that's what you need to do to enforce this good straight. No, it's just like you wouldn't ever like get past mac or expansion and type check, yeah. Yeah, the type of, yeah, you have, we'll get to that after this example, I'm just gonna, I'm just going in that direction, yeah, you, you what? Oh yeah, so you could say that ID is any valid positive integer and age is any positive integer. That's a built in numeric type, you can't say like even. I don't, I don't, I don't believe I can, I can actually create positive integer as a type, that's like something to do with how Racket is implemented in, in C, yeah. Now, yeah, and you couldn't have types for like infinite even integers, you can have like a Fibonacci number type, yeah. Okay, so let's say that actually 1 to 1000 actually is actually a valid ID for the second example. Okay, so that, that's fine. So we can't now, for instance, create an invalid student. We can't say that their ID is negative 12, that their age is, that their name is John, that their age is 100, that their faculty, we could, so we give them a valid, valid faculty in a valid term. But if we try to create this student now we get a type error. So like, you can't create invalid students and have your, your, your programs type checked. In the interpreter here, like it's, it's type checking like before, like at each line that you type into the interpreter, just like how you'd use this Scala, Ripple or something like that if you're miller, if that, but you couldn't have, you couldn't create like invalid students anywhere in your, in your program before it runs, it wouldn't type check now. Yeah. So that's that example. Okay. Now, what I want to do next is show you how to create a type for the piano numbers using structs, record types and type bracket, and then go on and show you do it with recursive types as well. Yeah, record type record supports recursive types, but they're kind of functionally the same as if you just kind of defined, for instance, in this case, piano numbers, how you would in Scala with like, for instance, with case classes and subtyping, one way you could do it. Yeah. So, so you could create a type, you could create a struct for NAT, a struct for zero, which is a subtype of NAT, a struct for S, which is a subtype of NAT, and takes a N, which is a NAT, which is its predecessor. And this would be like functionally the same as how you'd say that a NAT is either Zed or the zero or the successor of NAT in a programming language that supports algebraic data types like Haskell. Yeah. So, this is fine. This is similar to how you might create NATs with case classes and Scala and subtyping. I'm thinking there is a run is a command area. Okay. Yeah. Okay. So, you could say that you could, for instance, create zero, which is a subtype of NAT here. You can create the successor of the successor of zero, which would be say two in this case. But we run into this problem where oftentimes you just want to say that zero is a NAT, but it's a variant of NAT, and you don't always just want it to have the type NAT, or you could say that successor of successor of zero is a NAT, but you always wanted to be treated as the NAT type, and that successor of some natural number and zero are just variants of that type. You'd always just want it to be type when you're creating functions that use NAT. So, you wouldn't ever want to create a function that produces, or you might in some cases, but oftentimes you'd want to create a function that just gives you a NAT or takes a NAT and gives you a NAT rather than zero in the successor of NAT. And so, oftentimes because of subtyping, subtyping gets in the way of type inference here, that's my point. Like, if you just type Z, then because you have subtyping, it will infer that Z is the type here and not being a subtype of NAT and not NAT here. But this example here is also just some successor type rather than, which is a subtype of NAT rather than NAT. So, you have to explicitly annotate types and type track in many cases. So, you'd have to explicitly annotate that this is a NAT, that zero is a NAT somewhere in functions that are using natural numbers, using your piano numbers. You're right, I don't guard here, even though you can, I believe, yeah. So, you can guard structs and type track is saying that this can't be subtyped. But I wasn't going to go there for the sake of this example, but you're right, yeah. Or maybe I don't have the syntax quite right, but yeah, you can add a guard so that you can't subtype NAT outside of this module, yeah. So, what you're saying here is we want to be able to have a type and we want to say that a natural number is either zero with a successor or some natural number. And to do that, we need to first create a struct for NAT, which is like the, and then extend NAT and create zero. And then also have another subtype of NAT, which is the successor of some natural number, which is effectively saying that a natural number is either zero or the successor of some natural number. That's what we need to do to have this functionality and type bracket, yeah. I'm just confused by the initial line. That that says NAT is a struct with no elements? Yeah, it's just a struct that takes no fields, yeah. So, you don't have to create stuff there. You're right, I might even want to be more precise by enforcing the constraint that perhaps you can actually create a NAT, but you can create either zero or a successor, some natural number, yeah, yeah. So, we talked about record types and type bracket. Let's talk about parametric polymorphism in type bracket. You can have types and record types that take another type as a parameter to construct a new type. Let's, how many of you are familiar with the example of an option data type in Haskell or perhaps Scala? It's either, you have an option type that's either some of some type or it's nothing. It takes, for instance, you can have an option integer. It's either contains an integer or there's nothing there. And so to do this, we can create, again, we can create a struct for, we can use record types to create a struct for the none case. And then we can create a struct for the some case. And here's where we take the type parameter in this case, A, which could be, you give it some type, you create some and you put A inside of it, some value of type A inside of it. And then we define a type called option that's the either some or it's either none or some of A. You parameterize the option type here, too. Now, if you go back, you could actually create a type for NAT that's the union of Z or some of A where A always has to be a natural number with using define type instead of having a struct for NAT and then sub typing it. The second line where you define some, some of the name of the structure, so the syntax in this case for struct has the type parameter before the name? Yeah, that's the syntax in type record, yeah. Okay. And we want to effectively create what you might see as option say Haskell, which would be an algebraic data type that an option is either none or it's some of A. And that's how we effectively create this functionality in type bracket. Run this code. You could, for instance, create some of integer, an option of integers, I think I should put the type instead. Yeah, so we can give option the type parameter integer to create the type that's either none or some of integer. There's no support for higher kind of types in type bracket, which is one of my remarks that I think would be nice to try to add higher kind of types to type bracket. Where I'm going with this is I want to show you how you might add algebraic data types to type bracket in a sense just like how we created the syntax, how we made it so in some sense we can add range types to type bracket. How might we define syntax so you can create algebraic data types where you just say define data type option A, which is either none or some of A, and it creates these structs for you and does all the subtyping and guarding and whatnot, and then actually creates an option Pacific pattern matching construct so you can say instead of using match to match on these structures, you might have some function that if you have, it takes an option and if you give it some type do this or if it's none do that, you can use rackets pattern matching construct called match to destructure your option, but that's not safe in the sense that you can't provide full case coverage at compile time. You could have a function that only handles the sum of A case, and then if you give it none at runtime it fails. And so we want to, when we create these add algebraic data types to type bracket, we want to both make it easier to define data types like this so you don't have to define structs, you just say define data type option as either none or some of A, similar to how you would in Haskell, but also give you compile time case coverage by creating this type case construct behind the scenes where you can say type case option, my option, and then if you don't provide case coverage for both the sum of A case and the none case, then you don't type check, yeah, yeah. Now as an exercise, you might be familiar with the either data type in say Haskell, which is either the left of A or the right of A. Based on what I just showed you with the, for defining the option type in type bracket, how would you define either using structs? Yeah, it's a union. You define left and right, and then either is the union of some, like you'd be, I'll just show you the answer, yeah, you. I'm not sure I understand the example. What is the meaning of left of A and right of A? So an either data type lets you, for instance, create types where you can either have some, it allows you to branch but express how you're branching the types like you'd either have, like say, you complete some request and the result is either a successful transaction which would be left or some error which would be right and then you might make some decisions in your software based on whether or not you have one result from the result of a transaction or the other, but express that in your types before your program's run. That would be the application of that, yeah. So you'd create a struct for left which takes some type A and a value of that type A, and a struct for right which takes some type B and a value of type B, and then you define the either type which takes two type parameters A and B, and it's the union of either left of A or right of B. Yeah, so for example we could say what's the type of either string or error. I'm sorry, kid. Could you just say that right? Like alias right to left? Yeah, alias right to left. I don't think it creates a new type. Alias are just like, it would just expand to left. Oh, okay. Yeah. It's not like a new type, yeah. It's an alias, yeah. Except that you could call the parameter A here when you define left as a struct and call it A here for right, but you couldn't say define type either A and A, yeah. Oh, yeah. Yeah, it's unbound when you're just creating the struct, but you can't have two As in either, yeah. Yeah, this struct needs to take a type as a parameter to construct a type. Like just a left of A isn't a type, it's a type constructor, and you have to give it a type to create a type, yeah. Oh, yes? Yeah, you're creating a type.  I'm sorry, so you mean the define type? Yeah, you're aliasing either A, B to, I have two type parameters for this union type of left that takes a type parameter and right which takes a type parameter. Now, I don't think you can just have like, yeah, define type is a type alias.  Like actually, like you don't have, like see, if we print the type of either string or error, it's just the union of right error and left of string. Like there's no, it's not like a new type, it's just the union of right of error and left of string. It's just a name for that. It's an alias. Okay, and you can also have functions that take type parameters and racket to. For example, you can, in our type racket, say we had a chunk function which takes some list and a number. So if you had a list of say nine integers, or if you have a list of nine items and you wanted to chunk it into three, it would give you three chunks, the first three, the second three, and the last three, if it was eight, it would give you three, three, and two. And so, and we wanna type this function to be able to take a list of some type. You give it a type, so a list of say, a list of that type that you give it and then an integer and then it chunks that list of the type that you gave it. So it works for all lists. Yeah, lists of any type, yeah. So we give it an empty list. We want to, we wanna give back an empty list. If the length of our list is less than n, then we just wanna give the remainder of the list. Like I said, if you had, you'd get three, three, and two. If you gave it a list of eight items. Otherwise, we want to take the first and elements of our list, which would be a list and then chunk the rest. So it works like if we give it a list of nine items, you take the first chunk, which would be three, then you give the list of the remaining six and then it chunks it again and then chunks it the last time, then it's done. So how might we type this in? As I said, you can make, give functions type parameters and type brackets. So you could say that for all types a, sorry, this function takes a list of that type, a and an integer, or maybe I'll put this all in one line, and gives you a list of list of that type as a result. So our type signature, the type signature? Yeah. Yeah, so like our chunk function takes some type parameter. So for all types a, it takes a list of that type as input. So if you give it an integer, then it takes a list of integers and an integer and gives you a list of list of integer, like chunks your list of integers. If you give it some other type then it chunks a list of that type. It just works for a list of all types. I know, I don't think so enough. Yeah, I don't think you have existential types in type bracket. You mean like, like, sorry. I think it's bound to the function. So you could say I'll let some value of type a, b, this. Yeah, you can actually use the type a inside the function. For a, a survive. Yeah, a is bound, this type is bound, this type parameter is bound throughout the function. So like the function knows about the type a if you want to use it somewhere, yeah. So say we wanted to chunk a list of one, two, and three into pieces of two, then we would get, it infers the type of this list as positive byte. So it gives you a list of, list of list of positive bytes as a result. Type a here is inferred to be positive byte. But rather than giving you like a list of any when you parameterize the, you say that this function takes the type parameter. It doesn't just infer any, it gives you back a list of list of positive bytes. That's the idea. Now, again, like I said, sub-diving kind of gets in the way in type brackets. So you might want to say that explicitly that you're passing in a list of integers as input. And so I think if you said that one, two, and three is a list of integers and you want to chunk it into sizes of two, then it gives you a list of list of integers as a result because of sub-typing, you have to sometimes explicitly annotate what your input is. But it'll still say, it'll still infer that the type parameter A is integer. So you get a list of integers as a result instead of list of list of any, if you didn't have the type parameter, yeah. Show what, sorry? The command you just left. Oh yeah, sorry. So I first typed, after we made our chunk function, I showed that if you try to chunk list one, two, three, and two, it thinks that it infers that you're giving it a list of positive bytes. So it gives you a list of positive bytes as a result. But you might want to explicitly annotate that that list is a list of integers because you want to work with integers and not positive bytes. And so it infers that positive bytes is what you want, but that might not be what you want. And so you can have to sometimes explicitly annotate that it's a list of integers. I think that you'd rarely want to work with, if I just create a list of one, two, and three, I'm thinking in integers, like you're being precise by saying it's a list of positive bytes unless you had an element with, if you said one, two, three, and 30,000, it wouldn't think it's positive bytes because the range of positive bytes is like zero to 255. But if you're below that range, it thinks it's being most precise by saying that you're working in with positive bytes. Is it not most precise though? It is most precise. It is, I guess, strictly speaking, the most correct. Because you might be working with, you would have to coerce to integers at some point if you didn't want integers, and like if you were working with, if it inferred positive bytes and you want an integer. One off of this list. Absolutely. I believe, yeah, at some point, yeah. If you don't explicitly annotate what it is before passing it to the function, yeah. Okay, so let's talk about recursive types in type bracket. Okay, so like some, as some people mentioned, there are some types that are naturally defined recursively rather than using structs. I mean, you could define lists and the piano numbers using the struct and subtyping approach that we used, but it might be more natural to, for instance, let's actually start with the example of a binary tree. Like, binary tree is either, like it's either some leaf or it's a tree, or it's a binary tree. So you could define this type for binary trees. You actually, since we just talked about parametric polymorphism in type bracket, give this a type parameter. We're defining a type called binary tree, which takes a type parameter A, and says it's a recursive type, and we have to give that recursive type a name here to be able to recurse on it. We'll just call it what we're recursing on BT for binary tree. You can actually just call it binary tree or two, but BT is shorter. And say it's either an A or it's a pair, a vector in this case, of A and A. So it's either a leaf or a binary tree. Sorry, or it's two binary trees, it's plus, yeah. Yeah, so for all A, a binary tree is either a leaf or a pair of binary trees. Now, how might you define a type for quad trees based on what I just showed you? Yeah, more things in the vector, yeah. So are you suggesting we create a type for binary trees using structs, or you might make things that you actually tag with the fields area? So we define quad trees similarly by just saying that a quad tree is either A or it's a vector of four quad trees. Again, this is a type that, for all types A, you either say that a quad tree is either a leaf or a vector of four quad trees. So let's go back and look at, and define the piano numbers using recursive types and type bracket. You still have to create a struct for zero. And for the successor of some natural number, you actually, what you have to do is actually make that struct for S, take a type parameter, and say that the successor of some natural number is the successor of one of that type. And then you have to define a type for the piano numbers recursively, and say that piano number is either a natural number or it's either zero, or saying that a natural number is either zero or the successor of some natural number. It's called that ZZ, so we already have the, sorry, I'll actually get rid of our definition up above. We'll open up a new file. So we've defined this type for the natural numbers using recursive type constructors and type bracket, but functionally it's the same as how we just defined it using structs and type bracket. There's really no difference in terms of how it functions. It's just, I guess it's personal preference, whether or not you think it's more natural to define the piano numbers using that recursive type constructors, just use structs and subtyping. Because it's doing the same, it's still inferring because natural numbers is either the union of Z or some natural number, even if we define that recursively, Z and S are still subtypes of NAT here. We just don't say so when we define the struct, and there's no record type for struct for NAT. So you still have to explicitly annotate these Z and the successor of some natural number in many cases. If subtyping gets in the way of type inference. But let's define a function that uses this type for the natural numbers that we defined using recursive type constructors. Let's create a function that takes a NAT and gives you a number. So it goes from like our inductive definition of the natural numbers, piano numbers to an instance of number in racket. So it takes some natural number N. And now I'll introduce racket's pattern matching constructs. So we actually destructure our natural number that we pass as input when converting it to a number. And I'll show how you can't provide full case coverage here. Like we could leave out the case where we have zero and we want to convert zero to the number zero, like our zero in the natural numbers to like the racket's numeric zero. And how if you leave that case out, we can't provide full case coverage at compile time and we can have a runtime error in our program and cause it to fail. So if we match on N to provide full case coverage, we'd say, we'll call it NAT actually. And like it's either successor of N's some natural number. And in that case, we want to add one to NAT that it's a predecessor converted to a number. Or if we have zero, we want to produce the numeric number and type racket zero. It is, because like if it's, the successor of N is one more than N, yeah, yeah, yeah. And we can type annotate this function by saying that NAT to number takes our recursively defined natural number type and gives you a number. For instance, NAT to number of zero. Oh, sorry, we have to give it a NAT. Yeah, NAT to number is the name of the function and you can use that symbol in function names and in all identifier names and type racket, yeah. And racket, yeah. So for instance, like NAT to number of zero is the numeric number zero. The successor of zero is two. But we can do things like leave out the case where we handle zero and give you zero, which would be a mistake. But MATCH doesn't give us compile time case coverage for our recursively defined natural numbers type and type racket. So if I try to take the NAT number Z, now there's no case for that. So we can't provide coverage before our program runs where is with algebraic data types in what algebraic data types should be like in programming languages like Haskell is they should provide compile time case coverage. So any function that you use that you make decisions by pattern matching on that structure, you should have to provide full case coverage or else your program won't type check or compile, yeah. And that's what we want, I can't do that using MATCH in type racket. And where I'm going with this is how you might add algebraic data types to type racket and provide compile time case coverage by with this type case construct which is stronger than MATCH. You can't like destructure a NAT with conned. You can only do predicate tests. On type bracket, yeah. You could get a runtime error if you didn't have handle a case. Like if you just had one case in conned and you needed two. For some reason, yeah, it would just be a run. Yeah, you can't provide static coverage for that either. I'm sorry, so what we want to be able to do is like we know that a natural number, our representation of the natural numbers is either Z or the successor some natural number and we want to handle both the Z case and the successor of N case. And if we miss a case, we want to be able to make it so that we can't run our program, yeah. Oh yeah, that's where I'm going right now. So lastly, like the last big feature is the rackets type system which has been put into rackets type system to accommodate the style in which you'd program an untyped bracket where untyped bracket programmers like to do conned and then predicate tests inside your conned, like make decisions if you're input to some functions of string, they do this and if it's a number, then do that. It's called occurrence typing and like if you had say some function foo that you can give it either a string or an any and if you give it a string, if string or any is a string, then give you the string length of string or any, else just give you an error. Then with occurrence typing you can say that the type signature of this function foo is either you give it either a string or an any, the union of string any which I guess in this case which would just be any because any is the top type and it gives you either a string, either gives you an integer or error. So if you give foo three it gives you an error but if you give it success it gives you seven the length of success and that's occurrence typing. So do you have a question? Okay, so we've discussed the basic features we went over the features of type rackets type system and talked about how we type annotate previous examples of untyped racket code but one thing that's cool about type racket as I mentioned is that you can modify previously untyped racket, the idea is that you should be able to modify previously untyped racket code as little as possible and use it in type racket and have it type check it type check type racket inferring types wherever possible. And so if you go on the racket homepage and look at their example programs and untyped racket in many cases you can actually just change the language from racket to type track it and it will run it'll type check and run it'll infer what the type of this expression is and that's the idea. Yeah, you can explicit like if you, yeah you can explicit, you can require typed and untyped racket module and then say what the type signatures of every function that you want to use from that module is. Though there's efforts to type annotate untyped racket modules that people actually want to use and do use so that they're fully typed it's a typed version of that racket module in many cases shipped with type racket for example there's, you have like the JSON library and untyped racket for working with JSON objects for one reason or another. There's already typed JSON and I believe as an example but for instance in teaching people use the how to design programs module which gives you a bunch of functions and tools for creating shapes and sort of introducing racket to students through pictures. That's not typed yet but somebody's been working on typing that in their own like their own repository but it's not like in typed racket yet. I'm under the impression to the best of my knowledge that typed racket came first like the design and implementation of type scheme is sort of a paper that came from northeastern university like the guy who works there who works on type racket. Like I see I don't know enough about type closure to give you a mature answer to that question though I see from what I do know that type closure uses these ideas of like adding a currents typing to type closure so closure programmers might make decisions by doing predicate tests in the body of their definitions too and like in the type scheme paper written from northeastern university they introduced the idea for currents typing in that paper that's like their original idea so I'm assuming that type closure is founded on the ideas introduced in the type scheme paper in 2006 I believe yeah, yeah. So the last thing I wanted to talk to you about is how you might add algebraic data types to type racket so we saw how we could create these data types for option and either and our piano numbers in typed racket that was rather awkward to do so and we couldn't provide compile time case coverage for functions that make decisions by destructuring our piano numbers option and either. It was awkward to define as you mentioned we actually want to guard our say natural numbers Z and successor so you can't sub tape it after defining it so we want something to do that for us like ideally we want to be. Just can you do a nickel definition of algebraic data types so I know what we're. Algebraic data type is like a tagged it's where you, it's like where you can either have product types or tagged union types in the definition of your algebraic data types so you can have like this algebraic data types is X and Y it's a product of two integers like it's either an integer and integer or and then you can have unions say it's either both an integer and an integer for like a coordinate or it's the sum tag of a string like you have to tag your unions you know there are products or unions and type algebraic data types but you have to tag your unions so just like for option for example like we want to tag some or none instead of just having the union of nothing which would have no tag or just a if we didn't have tags then are we just be able to say that it's a we wouldn't be able to express that it either has nothing or it's or it's some of a what's really going on behind the scenes is just what we did with structs like that's what it is it's actually just the same though it's a kind of a nicer way to to express that yeah yeah so you want to be able to like say define data type Nat which is either the successor of a natural number or Zed rather than going jumping through the hoops that we that we jump through to to provide to to make structs to create create our representation of the natural numbers and want to be able to say define our NAT to number function again that takes a natural number and gives you a number but this time we want to enforce full compile time case coverage by so if we give it some number in NAT rather than using match we want to be we want to be safer by having this type case construct where we say we're doing a type case on a on a NAT and we give it our natural number NAT and if we give it the successor of N we want to add one to the natural number NAT to number if it's predecessor and if it's Zed we want it to be zero now Andrew Kent who's a graduate student at Indiana University has been doing just that adding algebraic data types to type bracket to make it easier to create our types for option either in and natural numbers provide compile time case coverage so I'll just for the sake of time I'll actually just show you this module here if you imported it creates macros for define data type and makes it so you can when you define a data type it also creates a a type case it creates like type case NAT which is specific to NAT and when you say type case NAT it looks up that that specific type case for NAT that gives you that enforces full time compile time case coverage for NAT so what you wrote before you wrote required data type doesn't work in type bracket now yeah like I'll link you to what Andrew's been working on but this is a module that you have to have to install I'll open it up now yeah so if you install this module with your from the command line like you'd use rackets packet man package manager like racco package install data type and then require data type after you finished installing it uh... then you should be able to uh... share the syntax right here my battleship rid of that then we have like compile time case coverage for a natural not to number function so on my bed so if we remove uh... like the case where we handle zero here and we try to run this this won't this won't touch it this won't you want to run your program no match happened at runtime so you're able to run the program and then try to map like give it zero and would fail at runtime and then say imagine some hypothetical scenario where your software would fail and a bunch of terrible things would happen because your software fail at runtime if you have compile time case coverage for NAT that's safer because you can't even run your program if you if you try to try to use NAT to number anywhere in your software before like it runs you just won't be able to run it you have to fix that first yeah you uh... yeah you need to you need to use you need to install data type yeah yeah so do raccoe package install data type raccoe yeah i think you might be able to do it in doctor racquet too yeah if you don't have it on your path like then it won't work um... profile yeah install package can you install data type from there yes you can install data type right inside doctor racquet okay so we we went over some basic features of type brackets type system saw how type bracket equips its type system with features that try to accommodate the style with that you program an untyped bracket to make uh... minimize friction when you're going from untyped bracket to type bracket i also show you how like we might want to uh... endow type brackets type system with some additional features that such as range types and algebraic data types that make it easier to enforce certain constraints that we might have in our software specifications and for instance provide compile time case coverage when we're pattern matching on these these uh... data types that we define rather than having the possibility of missing a case and having our software fail at runtime uh... as somebody mentioned like i i think it'd be great if we could explore adding algebraic data algebraic data i mean higher kind of types to type bracket uh... be able to like you know carry side effects side effects that are that our functions have and with types say that this function has some sort of i-o action or and what not uh... andrew the same guy who worked on the algebraic data types packages also working on dependent dependently type bracket exploring dependent types and type bracket i think it's it's it's all it's gonna be uh... icky situation if we're if we're just stapling a dependently type uh... type system on the untyped bracket like what like if we try to accommodate the style in which you program an untyped bracket and then have dependent types stapled on to that i i think that's asking for hypothetically bad things to happen like i think it's something along the lines of having a lot of situations where like you have undecidable type checking or weird things like that i don't know because we haven't like it nobody it's not really finished yet and we haven't i'd prefer to create a a language within racket because you you can have your own languages that that uh... like you could create dependent racket and have like a dependently type programming language with s expression syntax and and wouldn't you and you don't have to accommodate the style in which you program an untyped bracket you just have this uh... toy language within racket you say pound line dependent racket and just just play with that and that'd be great but i don't think we should try to like accommodate the style in which you program on type record for going in that direction it'd be a great teaching language to have dependent racket we shouldn't try to staple it on like it just should be a different teaching language that you use it some module and of course thank you any any concluding questions before we wrap up


The Marine Corps said farewell to its top enlisted leader and ushered in another at the Sergeant Major of the Marine Corps relief and appointment ceremony at Marine Barracks, Washington. Outgoing Sergeant Major of the Marine Corps Carlton Kent retired just weeks shy of 36 years of service. And I believe the Marine Corps will assist the product, assist the fighting army that the Marine Corps is in great shape for the next 20-some years because of great Marines that serve today. On a humid evening at the Corps' oldest post, the Commodon passed on the enlisted Reigns to Sergeant Major Michael Barrett, who asks Marines to keep their focus during the nation's ongoing conflicts. Continue to serve, continue to be selfless in everything that you do. Continue to do brave deeds and endure. You've got tough times ahead of us and we're going to need you. Barrett takes over as a 17th Sergeant Major of the Marine Corps. From Washington, I'm Sergeant Todd Hunter.


Beaches are structured by a combination of the waves and the sediment that's available for the beach. So waves redistribute sediment along a shoreline to produce beaches, and the dynamics of their interaction with the sea floor near the shoreline and coming up onto the shoreline shapes the sediment transport of beaches themselves. So waves move in the ocean and when they start interacting with the sediment surface there's a lot of friction and that friction is what causes the waves to break. The friction is slowing down the water flow speed at the bottom of the wave but the top of the wave keeps moving quickly and it over tops the bottom of the wave and that's how you get the turbulence. So one of the things that surfers know very well is that the topography offshore of a beach strongly influences the behavior of how and when those waves break. So when the waves break there's a lot of turbulence and so this zone in here is one where there's often erosion and there's a lot of force of the wave and the water flow moving on shore so a lot of the sediment that gets eroded during the breaker gets washed up the shoreline and the wave as it comes up is called the swash from the break. So the swash zone gets sediment transported onto it when the waves come up and then the sediment gets eroded back or transported back offshore as those waves retreat. The details of how much erosion and onshore transport you have versus offshore transport determines whether the beach is growing through time, it's stable through time or it's eroding away. And so that process of the waves breaking creates layers of sand on the beach that are about parallel to the topography of the beach. So as the size of the waves changes through time as the tides go up and down and storms come and go beaches end up changing their shape but in general the swash zone has approximately parallel layers they dip towards the ocean. As the waves change and erodes the beaches deposits on them but this is these parallel layers that dip towards the ocean are really common for beaches and a lot of times because the grain size varies a lot. There are often specific layers that are well sorted but between layers it can be different. So for example if you have very high waves you might end up with a granule beach whereas at a time during low waves you might end up depositing much finer grained maybe fine sand layers. Now there are times when you have particularly large waves associated with storms and tides and they create, they build up a berm. So the berm is usually created at the maximum height that the swash zone comes up. So this is the max, approximately the max swash reaches this area. So if you have a big wave that comes all the way up here it's likely to transport a lot of sand and then it will stop right here at this berm. And so the layers can extend all the way up into this area but only when you have the very strong waves. Occasionally the waves will actually top over the berm and you can accumulate sediment on the backside here as well. So the waves will be carrying sediment and they can erode as they start coming over the crest the water speed will increase again and they can transport sediment into the back berm area. And so while most of the beach deposits are in layers that are dipping towards the ocean there is this transition to a back berm deposit and if the beach migrates away it will leave this topographic high that is eventually called a beach ridge. So over time you have this deposition on shore but also some of this eroded sediment ends up going offshore and once it goes offshore the energy, the flow speeds are much lower and it becomes more and more difficult for that sand to get transported back on shore. Occasionally with large storm waves some of it might be but on average if you don't, if there's not a process that keeps supplying sand to the beaches they will erode away because there's the sink of sand offshore where the flow speeds are very low. Most areas with beaches the sand comes from rivers flowing in to the coast and then that sand is transported via long shore drift away from the river mouths and so it can be in one direction on the shoreline or it can be both but the beaches are intrinsically an environment that only holds sand temporarily. When humans do things like build dams that reduce the flow of sand into shorelines we're cutting off the supply of sand to maintain healthy beaches and without beaches having replenishment of sand whether it's natural or from humans they are not stable, they will erode through time with the transport of that sand into an offshore environment. Thanks for watching.


Welcome folks, we had the Dow industrials finished down at 618, NASDAQ off 277, S&Ps off 75, that was the downdraft inside the NASDAQ folks of 3.4% inside the S&Ps 2.5, and then the Dow industrials 2.3. Gold contract, gold contract caught a bid of $13.1340 an ounce and that's absolutely broke. It's down trend that's been going on since February. You had wide price spread, you got the volume behind the move, $13.65 is the number that it wants to go after, it's February swing high. Now that being said, silver didn't catch a bid, which is really unusual and that is divergence folks. Silver traded down to $14.66, that was trading into its strength, it did reject lower price, closed out at $14.78, this thing needs wide price spread and accelerated volume in order for it to break its downtrend, which it has not done yet. Oil, oil down $0.82, trading at $60.84, bottom line oil is building cars for lower price as is copper. Copper is down 5.5 pennies today, $2.71, it looks like $2.65 is game, notes and bonds higher price lower yield in a big way too. With a 10-year note, up 15 ticks, $124.14, 30-year bond up almost a full point, up 28 ticks, $149.17, they both are going after their highs and bottom line is that what you very well may get out here. I'll take a look at this, I'll put the 30-year up on a continuous contract and this very well could be a monster ABC structure on the way up. If we take this, we put this on a weekly basis. What you're going to see here is that we're basically going after the last high up there that $150.21, but the way this is actually trading, I think we can get up to about the $155.16, if we take a look at the 10-year, the 10-year right now is yielding $2.4, it looks like that wants to get out of $2.0. Big numbers, big numbers, Kingdoll rejected lower price out here today, that rejection however had volume behind the move, so Kingdoll more than likely is going to be right back downtown. We traded to a price point on a low to 96.810, you're at 97.135.


The Cube presents KubeCon and CloudNativeCon Europe 2022, brought to you by Red Hat, the CloudNative Computing Foundation and its ecosystem partners. Welcome to Valencia, Spain and KubeCon and CloudNativeCon Europe 2022. I'm your host, Keith Townsend, and we're getting to the end of the day, but the energy level has not subsided on the show floors. Still plenty of activity, plenty of folks talking. I have, as a second time guest, this KubeCon, which is unusual, but not, I don't think, disappointing in any way. We're going to have plenty of content for you on your, the CPO, or I'm guaranteeing you're the CPO of- Of defense. At defense. Yeah. We're going to shift the conversation a little bit. Let's talk about open source availability, open source security availability for everybody.  It lets me know when I'm steering into another lane. And I'm thinking, why isn't it just a standard thing on every vehicle? Isn't safety important? Think about that for open source security. Why is it open source security, like just this thing available to every project and product? I love that analogy, and thanks for having me back. We had a lot of fun yesterday. Yeah, we did. Yeah. At defense, we really believe security is something that everybody should benefit from because if applications aren't secure, if vulnerabilities find their way into production, then your mother, my aunt, uncle, using the internet, using an app, their identity is stolen through no fault of their own because the developer of that application didn't have access to the tools that he or she needed to secure the application. Security is built around public knowledge. When there are vulnerabilities, they're shared with the community. And we firmly believe that we should provide open source accessible tools that take that public knowledge and makes it easy for anybody to benefit from it. So at DeepFence, we've created a software platform. It's 100% open source called ThreatMapper. And the job of this platform is to scan your applications as they're running and find, identify, are there security vulnerabilities that have found their way into production? So we'll look for these vulnerabilities, we'll use the wisdom of the community to inform that, and we'll help you find the vulnerabilities and identify which ones you've got to fix first. So when you say use the wisdom of the community, usually one of the hard things to crack is the definitions, what we call virus definitions in the past. How do we identify the latest threats? And that's usually something that's locked behind value. How do you view that when it comes to open source? You're right, and it's worrying because some organizations will take that and they'll hide that extra value. And they'll only make it available to paying customers. Ethically, I think that's really wrong. That value is out there. It's just about getting it into hands of users, of developers. And what we will do is we'll take public feeds like the CVEs from the NVD, National Vulnerability Database. We'll take feeds from operating system vendors for language packs. And then we help organizations understand the context so they can unlock the value. The problem with security scanning is you find hundreds of thousands of false positives. Like in your SUV, as you drive down the street, there are hundreds of things that you could hit. But you don't hit any of them. They're false positives. You don't need to worry about them. It's the one that walks across the road that you've got to avoid you need to know about. We do the same with security vulnerabilities. We help you understand of these thousands of issues that might be present in your applications, which are the ones that are really important. Because developers, they're short of time. They can't fix everything. So we help them focus on the things that are going to give the biggest bang for their time. Not for the buck, because we're not charging them for it, but for their time. So when they invest time in improving security, the applications, we, with our open source, accessible projects, we help guide them to invest that as best as possible. So I'm a small developer. I lead a small project, just a couple of developers. I don't have a dedicated security person. What's my experience in adopting this open source solution? Am I biting off more than I can tune, creating too much overhead? We try and make it as easy as possible to consume.  And you've probably used tools already to check them and make sure that there aren't vulnerabilities. But nevertheless, you've got to let some of those vulnerable packages into production. And there could be issues that were disclosed after you scanned.  It's a daemon set. It's a one helm command to push it out. And that talks back to the console that you own, so everything stays with you. Nothing comes to us. We respect your privacy. And you can use that to then scan and inventory your applications any time you want and say, is this application still secure or are there new vulnerabilities disclosed recently that I didn't know about? And we make the user experience as easy as we can. We've had some fantastic chats on the demo booth here at KubeCon. And hey, if times were different, I'd love to have you across the booth and we'll click and see. The user experience is as quick and as sweet and as enjoyable as we can make it. All right, so we've had a nice casual chat up to this point. But we're going to flip the switch a little bit. I'm going to change personalities. It's almost like if you're a comic book fan, the incredible Hulk, Keith, the Mount Manor guy with the button up shirt. I'm going to unbutton my jacket. And we're going to get a little less formal, a little less formal, but a little bit more serious. And we're going to, in a second, start Kube plot. And you're going to give me the spill. You're going to go from open source to commercial. And you're going to try and convince me. In 60 seconds or less, you can, you can wait five seconds on the table and say you're done. Okay. That why, why you should do. Where's your challenge? Listen to it. Why you should listen to deep fence. Why should you listen to out defense? So I'm going to put the shot clock in my ear. So again, people never start on time. You need to use your whole 60 seconds. Start. Q clock. Keith, you build and deploy applications on Kubernetes or in the cloud. Your developers have ticked it off and signed it off saying it's saying they're secure, but do you know if they're still secure when they're running in production? With deep fence threat mapper, it's an open source tool. You can scan them. You can find the issues in those applications running in your production environment and prioritize them. So you know what to fix first. But Keith, you can't always fix them straight away. So deploy threat striker, our enterprise platform to then monitor those applications, see what's happening in real time. Is someone attacking them? Are they gaining control? And if we see the exploits happening, we will step in, tell you what's going on, and we can put the thumb on the attacker. We can stop them reaching the application by fire rolling just them. We can freeze the application so it restarts so you can go and investigate later. Five seconds. Be safe, shift left, but also secure on the right-hand side. That's it. I think you hit it out the park. Great job on... Cheers, Keith. Cheers. You did well on the pressure. The cube, we bring the values. We're separating the signal from the noise. 60 seconds, that's a great explanation. From Valencia, Spain, I'm Keith Townsend, and you're watching The Cube, the leader in high-tech coverage.


So, we have different domains. You might be a relativist in some, you may not be a relativist in others. So that's an important distinction, in which respect are you relativist? But there's also another dimension in which different forms of relativism can differ, and that will be important when we think about relativism in science. And this is now the idea that you can be a relativist in a methodological sense, and you can be a relativist in a substantive sense. Let me explain. When you are a relativist in a substantive sense, then you are a relativist in the sense in which I've talked about it up to this stage. Then you think certain judgments in certain domains systematically differ, and they differ with respect to background assumptions or cultures, and there's no way of ranking those in a neutral way. So that's what we've talked about this far, substantive relativism. But you may also be just a relativist in a methodological sense, which means that when you study a certain area, then you study this area with a methodology that is relativistic. So for example, if you are a relativist in anthropology, then you might approach the study of other cultures on the assumption that there is no way to tell in a systematic way whether the cultures' judgments say about oracles or about witches. Then you approach that discourse in this culture, the talk, the practices in this culture, without any value-tip stance. You approach the culture as if you were a relativist, as if there was no way of saying what they're doing is right or wrong. Even if though actually you do think they're wrong, you still approach them in your investigation without using the assumption that they are wrong. So let's just repeat this point once more just to make sure that you have fully grasped the difference. So let's say that we have an anthropologist who goes into a culture in which they have witchcraft or believe in witchcraft and they have certain practices around it. Say that they are trying to find out who are the witches amongst us. They are trying to persuade the witches to stop doing their witchcraft work or in this way trying to neutralize the witches.  Well, the most important thing about the relativist methodology will be is that you are trying to understand the coherence, the way in which the different assumptions of witchcraft fit together to form a harmonious whole without being contradictory in itself. You're trying to make sense of why do people think in this culture that witchcraft is a plausible way to think about the world as some aspect of their social world. That's the methodological relativism. You study witchcraft without actually evaluating it and you actually think that the evaluative stance might be standing between you and the proper understanding of the witchcraft in that culture. The relativist investigator will think that your best chance of understanding what these people actually think is not to immediately turn on your evaluative instincts when you investigate the culture. Someone who thinks that a relativist methodology is a bad idea will say, well, we need to understand why these people can have such false beliefs. How is it possible for people to believe such nonsense? Or what ideology? Or what deception makes it so that people believe these things? That's precisely the kind of approach that the relativist anthropologist will not want. Okay, so we've talked a lot about relativism in general. Not we have talked, I've talked a lot about relativism in general and then about the different forms it can take, but we haven't yet mentioned science very much. So let me now try to explain what we have gone over in very general terms to the case of science. Now, the kind of relativism that has been most controversial in the study of science over the last 30 years or so has been methodological relativism. And it has come not so much from philosophy of science, the relativistic methodology, as it has come from the sociology of science. But both philosophy of science and sociology of science are part of what in general one calls studies, science studies, or history and philosophy of science, history, philosophy and sociology of science. So philosophers of science constantly negotiate and argue and debate with the sociologist and with the historians. So let me say a few words of what the sociologists of science have done. And it's actually very fitting for me to be talking here in Edinburgh about the sociology of science, the relativistic sociology of science since that school was founded, started in Edinburgh in the 1960s and then flourished in the 70s and 80s. Key figures in this movement were and are people like David Bloor, Barry Barnes, then Stephen Shapin, Simon Sheffer in Cambridge, and Harry Collins and many others. Okay, so what did they do? I can make a direct link with what I've said about anthropology and what I will say about sociological study of science. Because the idea of the early work in the sociology of science was to say we should do with respect to science what the anthropologists are doing with respect to witchcraft. We should study the history of science not by asking how come those scientists in the past went so wrong in holding false beliefs that we no longer hold in science today, but we should rather try to understand scientific beliefs of the past against the background of the culture and the social arrangements prevalent in the cultures in which those scientific theories were developed. So the idea was let's take what we have learned from the anthropologists and turn the anthropological gaze on science. This meant that sociology of science was not declaring winners and losers. It meant when the sociology of science looked at episodes in the past the aim was not to say, look great, the correct view has won and let's celebrate this as so much of traditional history of science and indeed much of philosophy of science did do and still does today. But the aim was let's try to understand why certain scientific views come to become prevalent in a given time period and let's try to understand that against the background of what everything else people believed at the time. Let me give you a simple example that brings this home. Again, it's an example that links in two ways to Edinburgh. It links to Edinburgh because the historical case study I shall briefly summarize comes from a sociologist who was then based in Edinburgh, named Steve Shapen, but the historical case that Shapen studied is Edinburgh in the early 19th century. In the early 19th century, there was a particular form of physiology, stroke, psychology, popular in many places in Europe but particularly in Edinburgh and that was phrenology. Let me briefly explain the key assumptions of phrenology. Phrenologists wanted to explain differences between people. They wanted to explain why people differ in talents and they wanted to explain why different societies are organized in different ways. And to explain this, they stipulated a number of distinct faculties in the human mind and what was new there is that they were happy to stipulate a large number of such faculties. The traditional school philosophy that derived ultimately from Aristotle, from ancient philosophy and then was further developed in medieval times thought that there are about four to five faculties in the mind. There's judgment, there's the ability to form language, there's emotion and some other faculties that were distinguished. But a very small number. What was strikingly new about phrenology is that it stipulated, assumed, postulated a large number of such distinct faculties of the mind between 25 and 35. So, for example, the phrenologist had faculties for competitiveness, a special faculty that assumed was essential in the human mind and was responsible for our ability to judge our own standing in society, how we stand relative to other people, like the ability to scan whether one's social position is good or bad. That was an altogether new faculty in the mind that the phrenologist assumed. Then they also had faculties for musical abilities, they had faculties for different crafts that people might be able to do, they had faculties for different kinds of reasoning and much else besides. Additionally, the phrenologist linked the mind to the brain. The phrenologist thought that the different faculties that they distinguished each had their distinct organ in the brain. So they thought the brain wasn't just one thing, one organ, the brain they thought was a combination of many different organs and each such organ housed one of those faculties. Then they took a further step. They assumed that the size of the respective faculty or the degree to which one has one of the faculties is explained by the size of the organ. So if you are very musical, they assumed, then this organ that is responsible for music at the back of the head would be bigger than in people who only have slight musical faculties. And then comes the last step. They thought that the different development of the organs would reflect itself in different bumps on the human skull. They thought that the shape of the brain influences the shape of the skull and thus the phrenologist can read off the skull what someone's talents are. Now that sounds a quite bizarre theory to us today. So bear in mind that quite some influential contemporary forms of psychology also tend to think that the brain, not just the brain, but that the human mind has what's nowadays called a modular structure, a structure of parts that can operate to some extent separate from the others. Okay, but let's leave aside for the moment the parallels to today's use. At first sight it strikes us as a courageous theory, a bold theory. And one might think, so what explains that people believed that? And who wasn't who believed it? And who were the people who didn't believe it? Now comes the sociological analysis. So when Shapin analyzes this phenomenon of the popularity of phrenology in Edinburgh, he does not take the line of how can we explain that someone believed something so obscure. But he rather wants to explain why was it rational, perfectly rational, for people to be inclined to accept the phrenological views. Now the first thing that Shapin draws attention to is that phrenology actually very closely engaged with the human brain. Phrenologists were the first people to actually cut up the brain in very, very fine slices and produced big atlases in which they drew these details of the brain that they discovered by cutting the brain in very fine slices. So they engaged very closely with the empirical material. That's one thing that impressed a lot of people. But there were also other factors involved that pushed or pulled certain people in the direction of phrenology. And very important in Shapin's explanation here is the class conflict in Edinburgh at the time. Edinburgh at the end of the 18th and beginning of the 19th century experienced a great social change and upheaval. The traditional landed aristocracy was becoming more impoverished and there was a new class of people, tradesmen from the middle class or the bourgeoisie that were on the rise.  You had many, many new professions. You had a whole new division of labour in society. Whole new lines of trade and production suddenly sprung up. The response of the traditionalists, the response of the aristocrats was to say this new division of labour is unnatural. That's not how God has meant the world to be. The phrenologists said, no, no, that's exactly how God has wanted it to be and that God has wanted it to be this way. You can see from the fact that the human brain is such that it supports a high degree of division of labour. The structure of the brain supports the idea of specialization that we see in the society that is emerging in front of our eyes. Why is that? Well, God has made it so that there are many different faculties in the human brain and in the human mind and each of the faculty deserves its own specialized form of profession. That's the natural way to do it. The traditionalists said, no, that's not the natural way to do it. There are just four or five faculties in the mind and it wasn't meant to be that way, that we have all that specialization and division of labour. But the bourgeoisie thought that's what phrenology shows. Phrenology shows us that division of labour to the degree that we see in front of our eyes is natural. So let's step back of this and ask ourselves, what does that have to do with relativism? Let's just repeat the central message. Shapin is saying, when we study science and when we try to understand why certain scientific theories become accepted, it's not enough to look at the theories in isolation. It's not enough to just look at the evidence. What does the brain look like? And the theoretical beliefs. In this case, the brain has this structure of a combination of many organs. That's not enough to understand why a theory is developed in a certain way and to understand why a theory is accepted. We need to understand the whole scientific community in its social context. The social context of 19th century Edinburgh needs to be taken into account when we want to explain why phrenology became an important influential theory. So Shapin says, let's not evaluate phrenology. Let's try to explain why it became the dominant theory. So this is a methodological relativism. It's a relativism which says, in order to understand how science works, you had best not try to evaluate it at the same time. Of course you can have your evaluations, but don't keep your evaluations away from trying to explain why scientific theories become accepted.