Interesting that type parameters only make half a percent of difference. So for 2-3% of Python code, the equivalent statically typed code would get really hairy I assume?
I think it's analogous to generics in Go. Go left out generics, which isn't a problem for most code. But when you need it, it's super annoying not to have.
What features would a type system require to be able to soundly type check 100% of the patterns that are found in dynamically typed programs? Dependent types? Refinement types? Is it possible?
Occurrence typing, perhaps? (In addition to dependent types, rather than instead of them.) That is, the result of certain runtime tests can refine the type of an object.
It is impossible. Dynamically typed programs are able to look at the name of the type, write arbitrary Turing complete code reasoning about it, and then do whatever they want with it.
For example a unit test framework might walk your class hierarchy, identify all classes whose name matches a particular pattern, and then start doing stuff with that.
Of course there is always a way to accomplish the same thing without abusing the type system. But as soon as you do so, it is a different program.
That is not what btilly means. You are talking about using a type system to write an arbitrary program. btilly is talking about using an arbitrary program to specify the typing rules for a set of values. His assertion is correct: if you can use an arbitrary program to determine what the types are in your program, then figuring out the types of your program is undecidable.
Again, this is different from using a type system to write an arbitrary program. But, it is true that type systems which allow you to write arbitrary programs are undecidable. Because it's possible that such programs written in the type system cannot finish, then they cannot be well-typed. Most programs will be okay, and can be verified to be well-typed, but there still exist some that cannot be.
> That is not what btilly means. You are talking about using a type system to write an arbitrary program. btilly is talking about using an arbitrary program to specify the typing rules for a set of values. His assertion is correct: if you can use an arbitrary program to determine what the types are in your program, then figuring out the types of your program is undecidable.
Right, but my point is that it's not necessarily impossible to just express the program that figures out the type in the type system.
I'm not quite sure what you mean. Being able to "express the program" (which I take to mean a human writes the program) is independent of being able to statically verify what it does.
"Dynamic types are static types", so as long as you've got recursive types, union types and function types (and maybe subtypes, depending on the language) you can type check all dynamic programs. See section IX of Practical Foundations for Programming Languages or https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
If you did model, say, Python's type system in that way, it wouldn't buy you much. The real problem with dynamic types is that they're trivially true: all dynamic programs are well-typed and semantically meaningful. Any term which a human might point at and say "error" or "meaningless", a dynamic language considers to be a perfectly valid, semantically meaningful value. Sometimes those values are of a particular form, maybe with a name like "exception" or "error message", other times they might be unpredictable artefacts of arbitrary implementation details. There's no mechanism to tell such values apart from "proper" values (if there were, we would call that mechanism a "static type system", and violate our premise of dynamic types); even those values of an "exception" or "error" form may be perfectly valid components of a program, since they may be accepted as arguments, returned from functions, branched on, selected between, "thrown" (in the case of exceptions), etc.
If you did want to restrict the particular form of values in particular places (e.g. "the return value of this function should not have the form of an exception"), you can do that with dependent types. It wouldn't be pretty though, as you would have to manually transform those guarantees on your outputs into preconditions for your inputs; supply proofs of the guarantees, assuming the preconditions; have your callers guarantee to satisfy your preconditions; then repeat the process, over and over, until you reach back to the input/data-creation part of your program.
In my experience, that's basically the hardest way to use dynamic types. It's far easier to write distinct types with "correct by construction" invariants, rather than passing around brittle proof objects. Doing that would mean you're no longer "dynamic" though.
For example, consider the infamous vector type, used as the "hello world" of dependent types:
data Vector (t : Type) : (n : Nat) -> Type where
Nil : Vector 0 t
Cons : (n : Nat) -> t -> (Vector t n) -> Vector t (1+n)
A value of type "Vector Foo 5" contains 5 elements of type "Foo". To get the first element of such a vector, we can use "1+" in our type to completely rule out the empty case (since there is no Natural number before 0):
first : (t : Type) -> (n : Nat) -> Vector t (1+n) -> t
first (Cons _ x _) = x
Now let's consider dynamically typed values instead. The simplest way to model them is using tags:
data Tag : Type where
INT : Tag
STRING : Tag
BOOL : Tag
OBJECT : Tag
-- and so on for the fixed set of "dynamic types" our language has built-in
-- Turn "dynamic types" into static types
typeOf : Tag -> Type
typeOf INT = Int
typeOf STRING = String
typeOf Bool = Bool
-- and so on
-- Values of "dynamic type"
data Dynamic : Type where
Wrap : (t : Tag) -> (v : typeOf t) -> Dynamic
Unfortunately, since all we know about dynamic values is that they are "Dynamic", we have to keep track of all our knowledge about them separately:
getTag : Dynamic -> Tag
getTag (Wrap t _) = t
getValue : (d : Dynamic) -> typeOf (getTag d...
The article's spin is that since so little of the program uses complex features, we don't really need those features in our language. However this conclusion is not justified. The right question is how much more work it would take to write the program without those features.
The real use of this kind of work is studying how to best optimize dynamic programs. The conclusion is that a Python JIT optimizer can assume the first data type you see is likely to be what you'll always see, add a small sanity check for that case then goes down a fast path. This will correctly optimize 98% of the code. And there is nothing good to be done with the remaining 2%.
This is a concrete data point. JIT optimizers for other dynamic languages (particularly JavaScript) have discovered and taken advantage of similar things.
If 98% of the code has very basic types (i.e. function takes a Integer and returns a Decimal)... we could encode that in type hints with something like mypy, and get many of the type checking that statically typed languages get, without a crazy type system.
Hey I will take a 98% statically type checked language over 0%... if in so many cases I clearly know the types of stuff, let's put that info in there and detect and code time. So much of the standard library could use this to be cleaner.
Run a program while it is instrumented. The tool figures out what every type seems to be. Then goes back through the program and tries to prove that those types are correct.
It could then automatically annotate large chunks of code in a way that lets them run faster and will produce a warning if an unexpected type makes its way in in a future iteration. (An unexpected type, of course, being either a bug or a likely candidate for something that might expose latent bugs.)
That's basically how most JIT compilers work. But it would be nice to be able to get the annotations back out of the JIT. Anyone know of a JIT that lets you do that? (In any language, since now I'm just academically interested.) It that would be darned useful when one "inherits" a large, dynamically-typed code base... it would greatly increase freedom to refactor if you were more sure that such and such a function really does only ever get a number, despite all the code you see for handling objects and strings, for instance.
If I understand the article, a similar assertion would be: "Because multiple inheritance is used so infrequently, the onus is on the designers to show that the complexity is worthwhile"
That's obviously not true, though - these things add complexity to a codebase and are best avoided until the benefits they provide outweigh the increased cognitive load necessary to deal with them when something breaks.
I would intuit that if the more complex features of a language get very little use, then that's the sign of a more mature and thoughtful developer community that emphasizes readability and simplicity.
Not only this makes sense, Python offers pluggable type systems that let you type some of your program, or all of it - as much as you'd like.
A similar trend with TypeScript emerged in JS land where it's gaining traction. (and flowtype to some extent although that is seeing a lot less adoption)
> In simple terms, only 2.5% of call sites in most programs can't be handled by name-based typing with single inheritance. Adding parametric polymorphism (i.e., generics) only makes half a percent of difference, and most of the remaining cases can't be handled by widely-used mechanisms.
If parametric polymorphism only helps with 0.5% of all call sites, then probably:
(0) You're relying too much on implementation details across module boundaries. This destroys opportunities for type abstraction.
(1) You're unwittingly repeating the same logic over and over for multiple types. Not likely the case in Python.
(2) You're relying too much on unenforced conventions.
I wonder whether the authors consider "value = somedict.get('somekey')" or "match_object = re.search(pattern, somestring)" as returning a single type. Both of those common calls can return None.
I'm also curious as to what they consider "unbounded polymorphism". Calls like "len(s)" or "with cm" or "for x in s" work with many different types (though usually only on one type at a particular part of a program). Likewise, most of the collections types and classes are necessary generic (in one place you make make a set of integers and in another place you use a set of strings). The use of the collections is typically monomorphic but the collections themselves are necessarily generic.
Another thought is that when I write programs that use a single type for a given variable, I still place value on the duck-typing and polymorphism (to ease future maintenance, support debugging, and leave the code loosely coupled). For example, when I write a function that accepts a file object and the calling code only passes in file objects, I still value my ability to pass in a StringIO object instead.
Another thought is that I find the mechanical extraction of percent usage statistics to be dubious since the results are profoundly biased by the kind of code being sampled. For example, my data analytics code is nearly 100% monomorphic. However, code that uses ORMs like SQLAlchemy, Peewee, or Django or that uses templating engines (like Jinga2, Cheetah), or that does anything interesting would tend to have much different statistics. (Performance Guided Optimization in C has taught us that data and usage patterns greatly affect the statistics).
All that said, I don't disagree with the authors that a lot of Python code could be statically typed. Tracing JITs have already proven the value of call site specialization to a particular type.
I understood "unbounded polymorphism" to mean that for a given variable, it took on values whose types do not follow any structural rules. Your example with file objects and StringIO objects would not fall in that category, because their relationship could be modeled with single inheritance. (One from the other; both from a parent; both implementing an interface.) Nor would 'len(s)' be unbounded, because 'len' could be modeled as parametric polymorphism.
> I wonder whether the authors consider "value = somedict.get('somekey')" or "match_object = re.search(pattern, somestring)" as returning a single type. Both of those common calls can return None.
val get: 'a dict -> 'a -> 'b option
val search: re -> string -> match option
Above is an hypotetical type notation in OCaml for both functions. I think it pretty much covers everything.
> This doesn't mean that languages shouldn't include more complex type systems, but it does (or should) mean that the onus is on their designers to show that the complexity is worthwhile.
In general, the "complexity" of more advanced type systems is not presented to the programmer, with C++ being a notable exception.
Instead, the programmer benefits from ease of expression of types even when they are mostly writing monomorphic functions. For example, I would say that > 95% of the benefit I've ever derived from Haskell's static typing system has been due to the clarity of type expression and the codification of intentions in monomorphic functions! All the extra stuff with advanced type class features, higher order types, quantified types, etc., is nice and all, but it probably has only ever mattered to me for at most 5% of the cases.
Regardless though, in those other 95% of monomorphic cases, the clarity of the static type system, the way it has made me clarify my design and think about the type constraints in function call chains, the way it has made me codify my intentions for other developers to see, the way it has prevented silly bugs or highlighted misconceptions I wouldn't have otherwise caught -- this has all been very valuable, all without me ever having to really deal with any "complexity" of the Haskell type system. As a mere Haskell user, I don't have to fiddle with that. The existence of the fancier type options never gets in my way if I don't need it for anything.
Now, I love Python and I'm not saying static typing is always better. I'm just saying that if a language has a fancy and "complex" type system, that's not the same thing as saying that a day-to-day programmer will ever have to interact with that complexity in order to get benefits from it. They probably won't. They'll get lots of valuable benefits more or less for free even (perhaps especially) when their programs are mostly monomorphic.
26 comments
[ 1.9 ms ] story [ 85.0 ms ] threadFor example a unit test framework might walk your class hierarchy, identify all classes whose name matches a particular pattern, and then start doing stuff with that.
Of course there is always a way to accomplish the same thing without abusing the type system. But as soon as you do so, it is a different program.
Again, this is different from using a type system to write an arbitrary program. But, it is true that type systems which allow you to write arbitrary programs are undecidable. Because it's possible that such programs written in the type system cannot finish, then they cannot be well-typed. Most programs will be okay, and can be verified to be well-typed, but there still exist some that cannot be.
Right, but my point is that it's not necessarily impossible to just express the program that figures out the type in the type system.
If you did model, say, Python's type system in that way, it wouldn't buy you much. The real problem with dynamic types is that they're trivially true: all dynamic programs are well-typed and semantically meaningful. Any term which a human might point at and say "error" or "meaningless", a dynamic language considers to be a perfectly valid, semantically meaningful value. Sometimes those values are of a particular form, maybe with a name like "exception" or "error message", other times they might be unpredictable artefacts of arbitrary implementation details. There's no mechanism to tell such values apart from "proper" values (if there were, we would call that mechanism a "static type system", and violate our premise of dynamic types); even those values of an "exception" or "error" form may be perfectly valid components of a program, since they may be accepted as arguments, returned from functions, branched on, selected between, "thrown" (in the case of exceptions), etc.
If you did want to restrict the particular form of values in particular places (e.g. "the return value of this function should not have the form of an exception"), you can do that with dependent types. It wouldn't be pretty though, as you would have to manually transform those guarantees on your outputs into preconditions for your inputs; supply proofs of the guarantees, assuming the preconditions; have your callers guarantee to satisfy your preconditions; then repeat the process, over and over, until you reach back to the input/data-creation part of your program.
In my experience, that's basically the hardest way to use dynamic types. It's far easier to write distinct types with "correct by construction" invariants, rather than passing around brittle proof objects. Doing that would mean you're no longer "dynamic" though.
For example, consider the infamous vector type, used as the "hello world" of dependent types:
A value of type "Vector Foo 5" contains 5 elements of type "Foo". To get the first element of such a vector, we can use "1+" in our type to completely rule out the empty case (since there is no Natural number before 0): Now let's consider dynamically typed values instead. The simplest way to model them is using tags: Unfortunately, since all we know about dynamic values is that they are "Dynamic", we have to keep track of all our knowledge about them separately:The real use of this kind of work is studying how to best optimize dynamic programs. The conclusion is that a Python JIT optimizer can assume the first data type you see is likely to be what you'll always see, add a small sanity check for that case then goes down a fast path. This will correctly optimize 98% of the code. And there is nothing good to be done with the remaining 2%.
This is a concrete data point. JIT optimizers for other dynamic languages (particularly JavaScript) have discovered and taken advantage of similar things.
http://mypy-lang.org/
If 98% of the code has very basic types (i.e. function takes a Integer and returns a Decimal)... we could encode that in type hints with something like mypy, and get many of the type checking that statically typed languages get, without a crazy type system.
Hey I will take a 98% statically type checked language over 0%... if in so many cases I clearly know the types of stuff, let's put that info in there and detect and code time. So much of the standard library could use this to be cleaner.
Run a program while it is instrumented. The tool figures out what every type seems to be. Then goes back through the program and tries to prove that those types are correct.
It could then automatically annotate large chunks of code in a way that lets them run faster and will produce a warning if an unexpected type makes its way in in a future iteration. (An unexpected type, of course, being either a bug or a likely candidate for something that might expose latent bugs.)
https://github.com/python/mypy/blob/master/mypy/stubgen.py
Someone is already working on type inference using VM caches.
See http://forum.world.st/parameters-of-the-virtual-machine-td48...
If I understand the article, a similar assertion would be: "Because multiple inheritance is used so infrequently, the onus is on the designers to show that the complexity is worthwhile"
That's obviously not true, though - these things add complexity to a codebase and are best avoided until the benefits they provide outweigh the increased cognitive load necessary to deal with them when something breaks.
I would intuit that if the more complex features of a language get very little use, then that's the sign of a more mature and thoughtful developer community that emphasizes readability and simplicity.
A similar trend with TypeScript emerged in JS land where it's gaining traction. (and flowtype to some extent although that is seeing a lot less adoption)
If parametric polymorphism only helps with 0.5% of all call sites, then probably:
(0) You're relying too much on implementation details across module boundaries. This destroys opportunities for type abstraction.
(1) You're unwittingly repeating the same logic over and over for multiple types. Not likely the case in Python.
(2) You're relying too much on unenforced conventions.
I'm also curious as to what they consider "unbounded polymorphism". Calls like "len(s)" or "with cm" or "for x in s" work with many different types (though usually only on one type at a particular part of a program). Likewise, most of the collections types and classes are necessary generic (in one place you make make a set of integers and in another place you use a set of strings). The use of the collections is typically monomorphic but the collections themselves are necessarily generic.
Another thought is that when I write programs that use a single type for a given variable, I still place value on the duck-typing and polymorphism (to ease future maintenance, support debugging, and leave the code loosely coupled). For example, when I write a function that accepts a file object and the calling code only passes in file objects, I still value my ability to pass in a StringIO object instead.
Another thought is that I find the mechanical extraction of percent usage statistics to be dubious since the results are profoundly biased by the kind of code being sampled. For example, my data analytics code is nearly 100% monomorphic. However, code that uses ORMs like SQLAlchemy, Peewee, or Django or that uses templating engines (like Jinga2, Cheetah), or that does anything interesting would tend to have much different statistics. (Performance Guided Optimization in C has taught us that data and usage patterns greatly affect the statistics).
All that said, I don't disagree with the authors that a lot of Python code could be statically typed. Tracing JITs have already proven the value of call site specialization to a particular type.
> This doesn't mean that languages shouldn't include more complex type systems, but it does (or should) mean that the onus is on their designers to show that the complexity is worthwhile.
In general, the "complexity" of more advanced type systems is not presented to the programmer, with C++ being a notable exception.
Instead, the programmer benefits from ease of expression of types even when they are mostly writing monomorphic functions. For example, I would say that > 95% of the benefit I've ever derived from Haskell's static typing system has been due to the clarity of type expression and the codification of intentions in monomorphic functions! All the extra stuff with advanced type class features, higher order types, quantified types, etc., is nice and all, but it probably has only ever mattered to me for at most 5% of the cases.
Regardless though, in those other 95% of monomorphic cases, the clarity of the static type system, the way it has made me clarify my design and think about the type constraints in function call chains, the way it has made me codify my intentions for other developers to see, the way it has prevented silly bugs or highlighted misconceptions I wouldn't have otherwise caught -- this has all been very valuable, all without me ever having to really deal with any "complexity" of the Haskell type system. As a mere Haskell user, I don't have to fiddle with that. The existence of the fancier type options never gets in my way if I don't need it for anything.
Now, I love Python and I'm not saying static typing is always better. I'm just saying that if a language has a fancy and "complex" type system, that's not the same thing as saying that a day-to-day programmer will ever have to interact with that complexity in order to get benefits from it. They probably won't. They'll get lots of valuable benefits more or less for free even (perhaps especially) when their programs are mostly monomorphic.