So when Jamie Allen came to me and he was asking me if I wanted to come and speak at this, he told me to come up with a talk that was kind of good and provocative. I don't think he meant quite this provocative, but we're going to see what happens, because this is going to be interesting. I am, my job is to work on compilers. In my day job, I work on compilers. I design type systems. I've done research in type theory. So I'm very, very much an advocate of strong static typing. I love type systems, I think they're great.
But one of the things I think that gets overlooked in the zeal of the static typing community is that type systems are not an automatic win. There's a cost associated with static typing. There's a cost in terms of cognitive load. There's a cost in terms of time invested. And there's, obviously, compilation time and there's all sorts of things that factor into this, that you have to weigh.
And this talk is basically about some of the times where those costs maybe were not so worthwhile. Some examples of times where static typing fails on problems that have subtle complexity. Very, very common problems that have subtle complexity! And hopefully, through the course of this talk, we're going to gain a sense of some of the benefits and some of the downsides of static typing, some of the places where it fails. And also, maybe, we will learn a little bit more about static typing itself, right? Because learning more about type theory is always a good thing. And it's important to know these things. Feel free to heckle me throughout the talk. I imagine there's going to be a fair amount of controversy. So I hope you guys will, you know, pepper me with questions.
But before we start talking about some of the horror stories that you can find in type theory, we need to know what type theory is.
Okay, what is a type system? Well, this is a very complex topic, and so I'm just going to treat it essentially with a quote from Benjamin Pierce, who is coincidentally doing a talk in the next session that you should definitely touch. And he says that a type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
Now, there are things about this definition that you can quibble with, right? For example, is one part of this definition that a lot of people like to complain about. Scala's type system is not tractable. Haskell's type system, Agda's type system. There's a lot of type systems that are pretty much in arguably type systems, but are not tractable. So there's various things in here that you can complain about. But I think the essence of it is these three things right here. A type system is a syntactic method, a proof system that is based on kinds of value. Okay? We look at terms, syntactic terms, and then we look at the term, terms and we bucket those terms based on what sort of value. You might get out of them. Okay? That's what a type system does.
And it obviates certain classes of errors. This is the primary thing that a type system has to do. There's this notion in type theory of progress and preservation. These are two properties that every real type system needs to have that C doesn't have. These properties make up soundness. So progress and preservation basically tie the type system to the runtime system, and if you have them as a type system, then you can guarantee that any well-typed purpose, will not get stuck at runtime. You're never going to get into a situation where you evaluate or just doesn't know what to do. That's progress in preservation. But in and of itself, that's not all that type systems tend to be used for, right? Type systems are often used to encode other sorts of constraints, domain constraints. This whole notion of nominal typing, where you have a Foo of A and a Bar of A, and there are two different things, right? Fu of A is a constructor over here, and Bar of A is a construtor over there, and they're not the same type, even though they're just simple wrappers around A, right? Those are extra constraints that are not necessary to guarantee that the program is going to run to termination. They're not necessary to guarantee consistency. They are an extra constraint that's being encoded in the type system.
So type systems are often used to do those sorts of things. They often serve as syntactic documentation. You can find these sorts of things. They're almost like comments in the code at times. And they almost always require some form of upfront assertion. When you're putting those type annotations in your code, you are asserting that at this point, for this term, when this term evaluates, it will only ever give me these sorts of values, values that are in this set. Therefore, compiler go off and prove to me at compile time before I run it that there will never be anything but those values in this slot. This term will never produce anything but those values. This is an upfront assertion, and it's a cost that you do ahead of time. So these upfront assertions, this is where the cost of static typing shows up. Getting these assertions right is not always trivial.
Now, so far we've had two slides about what a type system is, and it really only scratches the surface. So I wanted to look at a perspective on type systems that isn't often examined in terms of practical programming, and that is the perspective of logic. So there is this notion in type theory called the Curry-Haward isomorphism. How many people have heard of that? Okay, a few of you. A few of you, good. So the Curry-Howard isomorphism basically says that there are concepts in type theory, basically every concept in type theory maps over into a concept in logic. Okay, and vice versa.
So the mapping kind of goes like this. Types are propositions. Types are basically theorems. They're hypotheses. You say, I think this is true, and you represent that as a type. Values prove those types. So if you write some declaration, right, and you say it has type foo, okay, you are hypothesizing that foo is true, that the proposition associated with foo is true. And that will be true if there is a value for foo, if there's a value for that term, if that term actually evaluates. It's important to note that terms themselves are not proofs. Some types of misconception, most literature on type theory glosses over this point. Terms are not proofs. Values are proofs. Terms are just evidence because in term, in Turing complete languages, you can have terms that don't produce values. Basically, any time you have a non-total language, you can have terms that don't produce values.
For example, if you have a function that is trivially recursive, deaf foo return foo, right? Foo just keeps running around in circles over and over and over and over and over again. And you can give foo any type you want. And you know what? It's going to be true because it's true in the sense that that's not invalid, right? It could just keep returning itself. But you're never going to have a value for that. Therefore, whatever type you're giving to foo is not necessarily proven. It's certainly not proven by foo because foo doesn't give you a value. It only gives you a term. So non-termination is the problem here.
The Curry-Howard Isomorphism defines a number of mappings here. So this is kind of, this is an example of some things here. So the unit type. The unit type is the traditional example of a type that is true because you can always get a value for it. If you have something of type unit, it's just trivial to get a value. Use the unit value. You have it right there. Similarly, the bottom type for all tau tau, that is false because you can never give me a value of all possible types. If you could do that, that would mean that all types are proven, therefore all statements are true and your logic is inconsistent. You can prove anything, but that's kind of useless. So unit is true, bottom is false, and we have some other correspondences, okay?
Arrow types, also known as function type, right? Function types correspond to implication. T1, arrow, T2, okay? T1 to T2, that function corresponds to the implication. If T1, then T2. Because if you have to you have to, have a value of type T, you apply the function to it and you get a value of type T2.
Product types, otherwise known as tuples. Tuples are and, right? Because you have to have both values, values of both types in order to get the product type. For some types, some types correspond to or. So this correspondence continues to extend, right?
You can extend this further on. Parametric polymorphism or generics, right? These are universally quantified types, and they correspond to universal quantification in predicate calculus. There's existential quantification. You have higher kinds, you can get higher order quantification. There's all sorts of fun things you can do with this. And a lot of research in modern type theory starts in logic theory and then works back into type theory, like Wadler's linear type, for example.
So this is a very, very, very strong correspondence. And it has led some people to say that to oppose types is to oppose logic. Well, I don't want to oppose logic. Well, I don't want to oppose logic. I like to consider myself a rationality. Person. But in practice, I find that type systems are confusing, restrictive, and annoying. This has just been my experience, right? They give me a lot of benefit, but a lot of the time, they're getting in my way in kind of painful things. And I keep telling myself, the pain is good, the pain is good, it will lead to enlightenment, and it's just not working anymore.
So here are some things that I have found that are problematic.
Numbers are a problem. And Eric is laughing for very good reason right now. It's funny because numbers shouldn't be a problem. Numbers are highly mathematical things, right? Obviously. And they really shouldn't be an issue. But we're faced with this fundamental problem. Computers are finite. We don't run on infinitely large memory bank. And by infinite, I mean truly uncountably infinite. We don't have infinite amounts of memory. You may think you have a lot of storage in your cluster. You don't. It's not infinite. It's bounded. And because it's bounded, we can't represent real numbers. There are also practical considerations, right? You want to be able to run your code in a reasonable amount of time. Your program has to run on real hardware. So, for reasons of practical speed, we have to make compromises, specifically in the area of precision.
And this is where things get really annoying, because precision is a runtime property of the number. Therefore, if you have different types for different precisions of numbers, right, that's a form of dependent typing. Okay? When you hear that phrase, train yourself to send a chill up your spine because it's really scary. Okay? There's people shaking their head right now. I find dependent typing very scary. And precision is a special case of dependent typing.
Precision types are scary when they're embedded within a language that doesn't have dependent typing because These languages don't have good tools for dealing with this situation. And it is surprisingly tricky to get this sort of thing right. Very, very, very, very, very, very, very tricky.
And you know what? We're just dealing with precision here. We're not even thinking about things like sign, okay? Positive or negative. That's a fundamental property of a number that the type system doesn't represent. Like, we don't even talk about it at the type level, but it's very, very important. And we're not dealing with it. We're only trying to deal with precision.
So where does precision fall apart.
Well, something like this. One plus two. Okay? We've got two integers, presumably. We're trying to go with that integer precision because then we can use 32-bit or 64-bit integers on your hardware and it'll be much faster. So you add these two things together and statically we can know that the result will be an integer. So far so good.
Decimals. 3.14 plus 2.72. Well, Well, technically, these aren't really decimals. I don't know exactly what they are, but they're sort of restricted precision decimals of some sort. I don't know. Remember, finite hardware. We don't actually have real numbers. So you add two decimals together. It sort of makes sense that the result would be a decimal. So far, so good. We're still within the realm of rational things, right?
Now we're getting into problem. Now we have a decimal and an integer. These are two different types. Okay. But naturally, we would want to be able to add them together, just like this. And by the way, notice, we're using the plus operator for all of these cases. So clearly the plus operator is being overloaded on different types. So there's your first sign of weirdness. Second side of weirdness. We're using it on two different types at the same time. And then we're producing something that's, I guess, a decimal type. So there's some sort of implicit widening going on. Like this is, we're starting to build up a lot of really scary cases here.
The other direction. Right? Decimal. This is pretty scary too. These cases are not symmetric because certain languages create operators as method calls. And so the first operand is sometimes magical or the second operand is sometimes magical. In the case of Ruby for example, this would be these additions would all be a dispatch, a single parameter dispatch on the fix-num or decimal class. Okay? So these cases are not symmetrical and they face slightly different problems.
And then there's division, which is really crazy, right? You take two integers and you divide them and the result is not an integer. I mean, it's not even a decimal, at least not a fixed decision decimal, but it's certainly not an integer. And, you know, what are, you know, how do we handle this in some sort of sane way?
Well, if you come from an object-oriented background, maybe your
first answer is subtyping. Solve all problems with subtyping.
java.lang.Number. Has anybody ever used that class to do
anything? OK, we've got a couple. That's amazing. I have never been able
to do anything useful with it. It's just like, OK, well, I've got a
number. I'm just going to cast it to something else, because I need to
get it out. So subtyping doesn't work.
Type classes work fairly well. Type classes for numbers, for the numeric tower, is something that Haskell does. And so we have this nice language, this very mathematical and pure language that we can look at to exemplify how this works out. But even Haskell, with all its purity, with all its academic niceness, it's still got some weird angles around how this all works. The way this type class notion works is you define your operations inside the type class. And if you're not familiar with the concept of a type class, it's basically a category for types.
class Num a where
(+) :: a -> a -> a
(-) :: a -> a -> a
negate :: a -> a
class Num a => Fractional a where
(/) :: a -> a -> aSo class num of A, okay? We're saying that there are some types that have the property of being a number. Okay, and if you are a type that has the property of being a number, then the plus operation is defined for you. Minus is defined, negate is defined. If you are a number, you could also be a fractional, in which case division is defined. And you'll notice that these are defined on same types, right? So you have a plus, right, requires two numbers of the same type and returns something of that type.
This kind of runs afoul of one of the things that we had on that previous slide, right? We were pointing out potential problems because we wanted to take 3.14 and add 2. 3.14 the decimal and add 2 the integer. And this requires that they're the same type. So something has to be happening that's extremely wonky.
And that's something that's happening is Haskell redefines what it means to be a numeric literal.
Prelude> :type 42
42 :: (Num t) => tThis type declaration here, so this is actually inside the GHCI console, I'm asking Haskell, what type do you think 42 is? And Haskell says, not integer, it says, well, it's some type T that happens to be a number. And we'll have to figure out what that is later. So that's a little confusing and weird. And it sometimes leads to some very, very strange amiguities. You try to use the div operator, for example. That's going to sometimes lead to strangeness as you run into conflicts between different types.
So that's weird. And not all the problems are solved yet. Okay? We still have issues with precision:
(1000 :: Int16) * (1000 :: Int16) = 169601,000 times 1,000. And I'm forcing these to be of type int16. Now my mental math is rusty, but I'm pretty sure that's not the right answer. So even Haskell is getting this wrong. Haskell gets it maybe arguably more right than Java, but it's still very wrong.
So numeric types, numeric types aren't catching everything. Numeric types are missing a tremendously large class of errors. You could argue that they're catching some things. They're catching some very, very basic things like adding integers and bullion, for example. But we're not catching the majority of things that we're interested in. And in the attempt to catch more things, in the attempt to make it better, we had to add a tremendously complex feature to the type system: type classes.
The notion of a type class is a very simple one, but they have very far-reaching implications across the entire type system. Type classes were originally added to Haskell to deal with the numeric tower. But there is a very far-reaching implication. But their addition has fundamentally shaped the evolution of the language and the community. Arguably in a good way, but it has had a fundamental effect. And this is something you're going to see time and time and time again with issues where language designers see problems with their type systems, and so they try to fix it by adding a feature to the type system.
And it doesn't matter how small that feature is. If you are fixing a case, a specific use case, by adding a feature to your type system, that is analogous to hunting rabbits with an atomic bomb. All right, the rabbit is dead, but there's a lot of collateral damage here. Okay, there's a lot of extra effects that are coming out of this. So type classes are a very, very heavy solution to this very particular problem.
And if you're interested to look at other solutions of this, F# has very specifically rejected type classes, and they have a magical numeric tower. So it'll be interesting to see kind of how that works out in practice. There are other languages that take different approaches as well that you can look at to see, you know, what sort of alternatives are there.
Numbers, some of the problems with numbers obviously have to do with the fact that we have preconceptions about how these operators should work, like we should be able to use plus everywhere. And that just has some really surprising results. But we can't just discount that, right? User expectations, and by user, I mean API user. User expectations are very important. It's easy when you're solving type problems, when you're trying to shuffle the types to make things line up, it's easy to get tunnel vision and just get focused in on, okay, I know that because of X, Y, and Z properties of type systems, it has to be exactly this way. Your user who comes to your API, not having seen X, Y, and Z, will look at that and be totally confused. And they'll be totally confused because you introduced complexity, you introduced rules and constraints that are not fundamental to the domain. So be very, very careful of that when you're doing design and you're solving problems in a statically type of context.
Can we do any better than this? I'm not really sure. Scheme seems to have a fairly nice numeric tower. But Scheme obviously is not statically typed. So I'm not really sure. I don't know if there are good answers to any of these problems that I'm raising. I'm just throwing them out there so we can think about it.
I specify object because I don't want us to be thinking about functional collections implementation. Functional collections APIs do not have these problems because functional collections APIs are tiny. And why are they tiny? Well, because just as a practical matter, you can't implement large functional collections API. You end up implementing a bazillion functions in a bazillion different cases, and it's just completely unmaintainable.
Scala's collections API has something on the order of a dozen or so collections, and every single collection has 70-ish utility functions on it. It's enormous. So 70 times 12 is a very, very, very large number. And it's not a number of functions that can be sanely maintained. So object-oriented languages kind of have an advantage in the area of large APIs, because they usually have some notion of implementation, or implementation inheritance of some sort.
And that allows you to have really nice collections APIs, really nice, large APIs in general but it introduces a large class of problems. The moment you open the Pandora's box of object orientation, you get into very strange waters.
So the very first thing that we need in order to be able to have a nice idiomatic object-oriented collections library, or really collections library at all, is we need polymorphism.
val xs: List[String] = List("foo", "bar")
val str: String = xs.headSpecifically, we need parametric polymorphism. Objectory into developers, when they think of the term polymorphism, they generally think of subtype polymorphism. Polymorphism is different. This is the thing that Java 3-1.5 didn't have. And so whenever you use Java Util List in 1.4 and earlier, you had to cast coming out of it. Well, casting is code for, I know better than my types of it. It's just shorter to type than that. So, parametric polymorphism makes this possible to express, right? You can have a list of string. And that's different from a list of integers. And when you pull something out of a list of strings, it's still a string. Fancy that!
But that's not the end of our woes. Okay? Object oriented languages have subtyping. And you would expect that this parametric polymorphism should respect subtyping. You may or may not like subtyping, but you generally have to admit that it's in the language. So you have to be able to deal with this case.
So here's an example, right?
def mkString(xs: List[AnyRef]): String =
xs.fold("") { _.toString + _ }
val strs = List("foo", "bar", "baz")
mkString(strs)We have this make string function that takes a list of AnyRef, which is, Sala speak for object. Okay? So we've got a list of any ref, and it does something to it and returns a result. We want to pass a list of string. Now, string extends any ref, so this should work, right? But in order to make this work, we need to have a feature called covariance. Okay? List needs to be covariant in its first parameter. And you need to be very, very, very, very, very, very, very, very very, very. careful with this, or you will end up with array store exception! So this is basically a problem that Java had in Java 1-0, is its arrays were covariant, but they did it badly, and they were warned about it, but they did it badly anyway, and it caused an actual crash, right? You could crash the VM in Java 1-0 just by doing bad things with your arrays.
You also, like, variants in and of itself, doesn't quite enough, because you can't actually use it. Okay? This is a problem that C# 4 developers are discovering as we speak. Variance in C# 4 is next to useless because you run into this problem: you're trying to define your list class, and your list class needs to have a pretend function that takes a value of type A and returns a list of A, right?
class List[+A] {
def prepend(a: A): List[A]
}Very, very intuitive, except it's wrong! It's not going to compile, and the reason it's not going to compile is A is covariant. A varies down with the class. Down with the type of A. Function parameters, like the parameter for prepend, vary contravariantly. They vary up. And so there's a conflict here. And if you don't deal with this conflict, if you just ignore it, if the compiler doesn't kick this out, then you literally end up with the problem that Java had with arrays. The reason that Java arrays are so horrible is because they ignore this problem.
So the way you have to fix it is with something called bounded quantification.
class List[+A] {
def prepend[B >: A](b: B): List[B]
}This is basically saying, in terms of Java generics, this is saying B super A. That's what it means. So bounded quantification. And this is basically declaration site variance with the plus A, declaring that A is covariance, and call site variance with the whole super thing, right, the B, super A. So we have declaration site and call site variance. And it's like really starting to spiral out of control.
But there's more!
There's more problems here. There's things we haven't addressed. Bitset.
val bs = BitSet(2, 7, 1, 4)
val ss = bs.map { _.toString }Bitset is a collection in the Scala standard library. A set that can only contain integers. Calling a map function on it, map is defined on bitset. It inherits it from set. And we say, for every element in this bit set, turn it into a string. Well, what is the result of this function?
Certainly not a bit set. It can't be a bitset, because bitsets only contain ints.
What should it be? Well, it sort of, I mean, it turns out that Scala is going to turn this into a set of strings, which is arguably the right thing to do, right? It's the most specific type that it could possibly be. But how did it know to turn it into a set of strings? Or conversely, how would you know to forbid this, right? I mean, the other option, rather than trying to do the smart thing, is you could make this a type error, and you could say at the static, at compile time, no, I'm not going to do this. I'm not going to let you map over a bit set with a function that returns a string. But how do you make that restriction? Well, you need something called functional dependencies.
Functional dependencies are a notion that comes out of Haskell. This is one of the developments that came out of type classes. And they require a lot of very clever trickery with type classes and how you resolve them.
So we've kind of got this laundry list of static type features that we're building up, that we have to satisfy in some way. We have variants. We have type classes with functional dependencies.
And it turns out that in order to have a functional dependency to resolve, to have a starting point for your resolution of your static typing, of your functional dependency, to know that you're currently in a bit set, we have to add path-dependent types. Bitset, the instance of bit set has to know that it's a bit set. And the only way to do that is with path-dependent types.
Now, path-dependent types are a generalization of existential types. So, we have parametric polymorphism which, as I said earlier, is universal quantification. Now we have existential quantification too. Existential quantification is the thing that hands out Fs in the predicate calculus courses in CompSci course. So this is probably a bad thing, right? Because all of us failed that exam. But we can't avoid it, right? We're just trying to do collection. We're just trying to have some very fundamental expressiveness to our collections. And we're running into these problems.
It turns out that declaring these sorts of collections, defining them is almost as difficult as describing what they do. This is the type signature for map:
def map[B, That](f: A => B)
(implicit bf: CanBuiltFrom[Repr, B, That]): ThatThis map is one of the simplest functions that you can have on a collection, right? It just takes a function from A to B and returns a new instance of that collection parameterized on B.
And if you squint, you can sort of see that in the middle there. But we've got all this stuff around it, right? We've got this can-build-from monstrosity with a Repr. I don't even know what a Repr is. And we've got a B and a That. I don't even see what type of collection we're returning here, because it's being computed for us.
And the Scala compiler basically needs all of this to declare the functional dependency, to be able to perform the computation at compile time to determine what your result type is going to be! And the way it does this is evident when we desugar it.
val ss = bs.map { _.toString }
(bs: BitSet)
.map({ i: Int => s.toString: String })
(cbf: CanBuildFrom[BitSet, String, Set[String]])So this is the map call, okay, and I've sort of put types on everything, so you can see what's going on here. So we've got BS, which is a type bit set. We're mapping with a function that takes an int and returns a string, and then there's this can build from, which has the bit set, a string, and a set of strings as its three parameters. Well, Scala needs to find this can build from. It's an implicit can build from. So it needs to look around to see if it can get it. This is how functional dependencies are resolved.
So the obvious question is, where does it look? Well, it starts by looking on Bitset. Specifically, it looks on the companion object for Bitset, which is very helpfully called Bitset. And it looks on that companion object for a can build from, that has a bit set and a string as its first two parameters. And it doesn't find one. So it moves on. It looks at int. Well, the companion object for int certainly doesn't know anything about Can Build From, and if it did, I would be terrified. So it moves on to string. String doesn't know anything about Can Build from either. It looks at Can Build From. Does Can Build From know anything specifically about Bitset? Well, no, thankfully.
So it goes back and it realizes, hey, I know, BitSet extends set. And can build from happens to be contravariant in its first parameter. Therefore, we should look at the companion object for set. Well, we go and we look at the companion object for set, like 17 steps into this resolution process, and we finally find a can build from which satisfies this signature.
And we weren't even done yet. There are nearly twice as many places as that, that the sky compiler will continue looking if it can find a can build from to see if it can satisfy this signature. And all of those places, all of those resolution strategies needed to be systematically added to make the collections library work. It's just really, really crazy.
So collections highlight a lot of weirdness in object orientation. They highlight some strengths in that you can have this very powerful and very flexible and you know, very useful collections library, but they highlight a lot of weirdness with this subtyping madness here and the different ways that you can call things. And it's very, very weird.
And it's very, very hard to get these things right. Martin Oderski, creator of Scala, really smart guy. It took him two years and four complete rewrites of the collections library to get it right.
Think about that for a second.
Two years to get it right. That's a lot of time.
As a side note, you're not crashing your VM anymore in Java because the VM now throws an exception if you get it wrong, but you have to catch that exception though. And the Java collections library doesn't have this problem with variance because Java generics are strictly invariant at the declaration site. Have you ever noticed how hard it is to use generics in Java? So the, I mean, Java's collections library doesn't have this problem because Java's collections library is impotent. Java's collections library has, gives you almost nothing.
Like think about it, you have a list, okay? You have an instance of Java Util List. What can you do with that? Well, I can put something into it and I can pull something out of it, and that's about it. It's like a dumb container that has some notion of ordering. It doesn't even give you any complexity guarantee because it is categorically impossible to do that in Java. You will find yourself running into these cases more frequently than you think. Perhaps instead of bit set, perhaps I should have used map. Okay? If I map, if I use the map function on a collection of type map, the elements it gives me will be tuples, key value pairs. Now, what if I return strings from that map function? Well, it can't put it back into a map because maps can't contain just strings. They have to contain a key and a value. They have to have two different things. So what do you return at that point? You know well, the only way to figure it out or forbid it, right? So those are the two options. Yeah, the only way to do either of those is to have functional dependency. Or to just kick out variants in your collections altogether.
So doing it at runtime is really easy. So doing it at runtime is really easy. So this is purely a compile time question. And the question is is how do you convince, how do you instruct the type system, how to figure out what the result type is based on this other type? You have a function that you want to run at the type level to determine what these types are. And that is actually the minimal definition of a functional dependence.
Could I solve it with type classes as well? Well, yes, actually, that's what Can Build From is. Can Build From is a type class. It's a very, very fancy type class that encodes functional dependency. So if you wanted to go further with it, right, you could do the entire collections library using typeclass. But if you do that, then you don't have any implementation sharing.
Well, the problem with functor is that functor assumes that you just have one type there. The target type, the thing that you're functing is… Right, exactly. So you're basically assuming no subtyping. Yes, so that's a runarish assumption.
Clojure screws with your collections types. It could do a lot better because Clojure is a dynamic language. I mean, all of this, all of this is really easy if you don't have a static type system. I think that's kind of my point. Like, if you're in a dynamic language, this is trivial. Because what is the appropriate method to use? I mean, if I'm going to construct an object in particular type, dynamic or something.
And like, yes, you have to find the implementation of the function, taking into account subtyping, at runtime too, but that's a lot easier. So when you're doing the map function, a hypothetical implementation might be, you start mapping over your bitset, right? The first time you call that function, you're going to see what does that function return? Like do a dynamic check on that type. And then you're going to try to construct a bit set using some sort of factory that you can get from the bitset self instance itself. And you're going to see, can you use integers, right? There's going to be some sort of check, some sort of dynamic instance of check based on that. And on that very first element, which is a string, the bit set is going to say, no, I can't construct myself using integers. Try something else. Go to my superclass. And the superclass, which is set, is going to be able to construct itself using strings. And so that's how it would fall out. I mean, that's how I would do it in a dynamic language. That's an alternative. It's just much, much easier because you have runtime level tools. You have if statements at the runtime. You have method calls. You have all these tools that the runtime gives you that the type system doesn't.
If you are willing to relax what your type system is telling you, then these problems do go away. But how far do you take that? If you just take that to its natural extreme, then the type system isn't telling you anything anymore.
I think that making everything object is not the answer, because then you're casting everywhere, and you have no type system. It's just totally dynamic.
I think the alternative is there's no type system in certain regions. There are certain times, there are certain problems where it makes sense to allow things to be born dynamic. And there are languages that are exploring this now. Phantom, for example, and C# has a dynamic type that you can work with. That basically it's like having everything be an object, or at least everything that is in this slot, is an object potentially, and you can call it just without casting. And so you're essentially, it's a kind of a pragmatic choice where you're saying that, you know, I can't, my type system isn't going to work everywhere. So I'm going to give you this escape hat where you can say, okay, do whatever it is you need to do and then come back to the type system when you feel you're ready.
Audience member: So yes, so as you relax your types, you can't go back. You've thrown away the ability to prove it at a point.
You've thrown away the ability to prove it within a certain region. You are, you enter this region, and you lose your ability to prove things in this region, and then you come out of that region and you assert "it's a string." It is a runtime assertion, but that runtime assertion guarantees that an exception will be thrown if it's not that. And from that point forward, everything is proven. Yeah, everything is proven from that point. It's just within a particular region.
And this is superior, actually, to what we have right now, where we have to send things to be object, and then we have to be super explicit about mucking things around until we get to the right point. So C# dynamic is actually a more more controlled way to escape the static typing than what we have at present.
So, remember early on in the top, we talked about the Curry-Hawood isomorphism, and I said that, you know, Paul Sidivly says that to oppose types is to oppose logic. And then we had just seen all these examples where types are kind of annoying.
I mean, I don't know about you guys, but at this point, I kind of want to oppose types. But, you know, oppose types is opposed logic.
Well, this turns out not to be exactly true, which is kind of saving us a little bit. So let's think about what this means. A program without types. And you can make this more specific, right? You can say a region without types. Okay, so a program without type. So what is this in terms of the Curry-Hawood isomorph? It is a proof without propositions.
There's nothing actually illogical about that. It's a little odd, but it's not actually illogical. So if you are coming at this from a perspective of formal rigor, Okay. Formal rigor and provable systems and things like that, you needn't be afraid of dynamic typing, because dynamic typing is not illogical. It's not, it's weird sometimes, but it's not illogical at all. So it's not something you have to be worried about using.
And just in general, right, we work with non-total languages. And so there are classes of errors that we miss. And so just as a general rule, types confer very, very narrow benefit. There's a very, very narrow class of problems that you can solve with static typing, the very narrow class of errors that are being removed from your field of view.
I don't agree with everything that Rich Hickey says. But one of the things that he has said in the past, which I think is kind of funny, is he says that modern static type systems are like putting guardrails on a sidewalk. Okay? Well, it's not hard to stay on the sidewalk. Very few people worry about that. So static type systems impose all of this burden and things like collections and numbers, and I actually didn't even show you guys functions, right? It's not just object-oriented languages that have this problem. There's problems with typing functions as well. And they require all of this effort for comparatively minimal gain.
And it's very, very important that we consider the trade-offs. Is it worth putting in all of this effort to make your types line up? Is it worth putting in all of this effort to strongly assert this thing at this point and this thing at this point? Well, maybe. Maybe that's true. Maybe it's not true. You need to decide. More importantly, you need to ask the question.
So what happens if we don't do static type? What happens if we go in a dynamically typed setting, right? Some of us have never used a dynamically typed language and maybe that thought of working without a static type system is a little scary. Well, what happens? You're code is often harder to maintain. Okay? You know, you can build it up very quickly, and it's easy to change things, but you don't have any guarantees that when you change this, something bizarre over here is not going to break. So you have to refactor a little more carefully, right? You have to have more comprehensive test suites to catch a whole class of errors that you otherwise didn't have to worry about. And you have to work things very incrementally and iteratively. Sometimes that makes things harder. Sometimes not, but sometimes it makes it harder.
More importantly, when you go with dynamic typing, your focus is on the runtime.
Let's think about what that means.
All of us, well, almost all of us, are paid to do programming, right? Okay? And people are paying us, presumably, to make the types line up. Right?
No!
They're paying us for the runtime. They're paying us for what happens at the runtime. They don't care if it's statically typed. Completely a development artifact. And so if you are spending all of your time – and by extension, all of their money – on making the types line up, that's a waste of time. Okay? If you're spending all of that time on making the types line up for comparatively marginal benefits, that's time you could have spent on the runtime. Maybe it would have been better spent on the runtime.
So it's an important question to ask, important thought to realize, and it's important not to be afraid to ask this question. Do I need dynamic typing here? Yes or no? Ask that question every time you look at things.
So we need to weigh the cost-benefit ratio.
We need languages that allow us to weigh the cost-benefit ratios and use these different tools as appropriate.
I didn't have this point up here, but I think it's very, very important. There are some modern languages, like I mentioned C# 4 and Phantom, that have support for dynamic region, where in a particular region you go dynamically typed with this particular value, and you do things with it that would have been hard to reason about statically. You do your thing, you do your thing, and bam, you're back in the world of static type. That seems to be a really, really nice solution, at least to my way of thinking, because it gives you the flexibility to make that decision.
So some concepts, just not amenable to static typing, they're very, very difficult to type. Numbers, collections, functions, the functions, you know, that example that I just skipped over, they're just not amenable to that. And type systems are incredibly complex, incredibly mind-staggeringly complex. They're a huge, gigantic solution. They're useful. Don't get me wrong. Type systems are very, very useful sometimes. But they're not very useful at other times. And we need to understand what that means. So I think we've got just a little bit of time here for questions.
So, Intellisense and really good IDE tooling. You know, we use Java tooling, right? And we sort of get this impression that these tools and these, these features rely on static typing. Might I remind everyone that the very first IDE was for a dynamic language? Smalltalk. In fact, arguably the best IDE ever created was for a dynamic language. So there are these tools that are out there. Ruby, for example, has some fantastic tooling built up around it that gives you Intellescent, that gives you refactoring, and all of these things that you would expect. I highly recommend looking at the NetBeans Ruby toolkit. It's really, really, really good. There's some really good tooling for JavaScript out there now as well that offers many of these same benefits. So there's nothing specifically about dynamic typing that makes that impossible, just occasionally harder.
So you do lose some performance if you go dynamic typing just as a consequence of how many languages tend to be implemented, right? Numbers, for example. If you don't statically know that this is an integer, you can lose some things. But you lose less than you would think. Ridiculously clever people working for Google right now that are making a certain runtime for a certain dynamic language that is blisteringly fast and getting faster by the minute. So, and if you think about it, a lot of things like assembly is dynamically typed. So there's nothing inherently slow. Okay, it's untyped. Either way, it's not statically typed. And there's nothing inherently slow about dynamic typing. Just sometimes your tooling, your platform has to work a little bit harder.