I dont like this paper. It makes statements based on references to opinion style articles. F.ex
"in practice, run-time type errors in deployed programs are exceedingly rare [TW07]."
If we look at [TW07] they state that
"even very simple approaches to testing capture virtually all, if not all, the errors that a static
type system would capture."
But provides no data or reference for that statement.
Another isue is that some references with data are based on small samples and possibly oudated:
"they [dynamc languages] lower development costs [Ous98]"
[Ous98] Compares time-to-implement and code-size for 8 different programs implemented in static and dynamic languages and shows that the dynamic languages are supperior. It is however not clear how much actual implementation is involved, so it may be the case that the difference is caused by diferences in available libraries at the time. In any case, the sample size is small and the article is old (1998) so it is not reasonable to make generalisations for programming in 2009 (or 20014).
Informally, dynamically types languages are chosen when the programmer prefers to get something running before getting something running correctly. Why would we assume then that once a program is running, the programmer would "find religion" and do the extra work to write a comprehensive test suite? If the programmer is willing to do work in an effort to prove correctness, the programmer would choose the far more efficient technique of rewriting the program in a statically typed language.
A dynamically typed program by its very nature a prototype, a program that is expected to fail when exposed to a non-trivial input. In many cases, that is fine, just not when correctness over many invocations actually matters.
> Informally, dynamically types languages are chosen when the programmer prefers to get something running before getting something running correctly.
I don't think that's at all true. I think that a major motive for choosing dynamic programming languages is that programmers want to get things running correctly and spend more time on the logic and less on making ritual invocations to the type system that are redundant with other elements of the code. (Haskell and other similar languages with very strong type inference are making this a less compelling reason to choose a dynamic language, but I think it remains an important one for many real decisions, as Haskell hasn't yet acheived the ecosystem and mind-share where its always likely to be considered as an alternative, and not rejected for reasons other than its type system.)
I think people who choose static languages do so because of concerns for correctness, but I think it is a mistake to reverse that to conclude that those who choose dynamic languages do so because they aren't concerned with correctness; many do so because the hoops you need to jump through in mainstream static languages are perceived as being a too-expensive way to get the (often very limited, given the lack of expressiveness in the type systems in many popular static languages) help in correctness that the static nature of the language provides.
I think that programmers reasons for choosing a specific language are as varied as the languages.
Personally I like programming in C++ because the typesystem and abstraction mechanisms allows me to write reasonably correct and concise code and at the same time performance is predictable.
I like programming in Python because of the emphasis on readability, the "batteries included" standard library and the scripting capabilities.
Both languages have failings, as do all the other I have tried, but what matters most (for me) is availability (platform support, libraries etc), which is the reason I occasionally write php code.
Robert Harper argues that dynamically typed languages are languages of a single Type:
And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice!http://existentialtype.wordpress.com/2011/03/19/dynamic-lang...
Bob in this same article also wrote the now oft quoted:
To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped.
Now the author of the linked article wrote another piece in 2012 that rebuts this:
It therefore makes no sense to say that a language is unityped without qualifying whether that relates to its static or dynamic type system. Python, for example, is statically unityped and dynamically multityped; C is statically multityped and dynamically unityped; and Haskell is statically and dynamically multityped. Although it's a somewhat minor point, one can argue (with a little hand waving) that many assembly languages are both statically and dynamically unityped.
Sam Tobin-Hochstadt argues the uni-typed classification is not very informative in practice.
The uni-typed theory reveals little about the nature of programming in a dynamically typed language; it's mainly useful for justifying the existence of "dynamic" types in type theory.
Another way to look at it is that the "uni-typed" pejorative assumes that types are intrinsic to the semantics of a language. Optional type systems reflect the reverse -- that types are an extrinsic feature that should be taken care of by an external library, potentially allowing the choice between multiple competing type checkers or no type checker at all.
The "unityped" descriptor is not meant to be pejorative. It's an observation that, from a type-theoretic point of view every expression in an untyped language can be given the same type. In a dynamically checked language, the type is the sum of all possible dynamic types (in Lua, for example: [1]). In an unchecked language, the type can be something else (in BCPL, for example, it's simply word; in the untyped lambda calculus, it's function). It's important to note that, according to type theory, types are a syntactic feature, not a semantic one.
It's just an observation rather than a judgment, and -- again from a type-theoretic perspective -- it's true. It's nothing to be offended about!
Note that if you were to write a type checker for a unityped language, then every program would trivially type check. So, while technically accurate, the notion of a language being "unityped" is not very useful. It's more of an intellectual curiosity than anything.
You may not mean it as a pejorative, but it's clear that Harper did, and so do those who adopt the term as a rhetorical device. I also have to question your use of the phrase "according to type theory". You are implying that there is a single type theory with a single view on the nature of types. I recommend the link I put in my previous comment.
Harper is frequently pejorative. He's also accurate. He has an agenda and it is difficult to interpret him unbiasedly without accounting for it. But if you achieve it then you realize you can no longer argue with the factual points he makes.
That said, it's a completely true point in the notion of "static-types-as-type-theory-defines-them" that dynamic typing is a mode of use of static typing which is completely captured in large (potentially infinite/anonymous) sums. Doing this gives dynamic languages a rich calculus.
Refusing to doesn't strip them of that calculus, it just declares that you're either not willing to use it or not willing to admit you're using it. Both of which are fine by me, but occasionally treated pejoratively because... well, it's not quite clear why you would do such a thing. There's benefit with no cost.
Then sometimes people extend this to a lack of clarity about why you don't adopt richer types. Here, at least, there's a clear line to cross as you begin to have to pay.
---
The "Church view" and "Curry view" are psychological—the Wikipedia article even stresses this! So, sure, you can take whatever view you like.
But at the end of the day type systems satisfy theories. Or they don't. That satisfaction/proof is an essential detail extrinsic to your Churchiness or Curritude.
Can you elaborate a bit on what the benefits of embracing that calculus are? Or maybe provide some pointers? I'm having trouble imagining what utility there is in treating untyped languages as (uni)typed. I said in another comment that it's pretty much a useless notion, but I'm genuinely curious if I'm overlooking something.
Probably the best one I can think of is that it gives you a natural way of looking at gradual typing. Doing gradual typing well is still tough, but you can see it as an obvious consequence of the unityping argument.
The article you linked makes little sense to me. They do mention Clojure's core.typed as an example of the "Curry perspective", as opposed to the "Church perspective", so I decided to check that out.
The core.typed user guide and it uses the same definition[1] of type that I'm familiar with from "Church" type theory. It even makes the same observation that Clojure is unityped! It seems to me that core.typed does not use a "different" type theory at all. Rather, it is a testament to the great extensibility of the Lisps that a type system can be bolted on as a library. Perhaps unfortunately, most languages are not so flexible.
P.S.: I re-read Harper's original unitype article, and it does seem pretty combative. I still don't consider the term pejorative myself. I dislike the term, but because of its lack of utility above any other reason.
I appreciate your coverage on type systems. One thing I want to point out is type systems are "a way" to model an information system. Type systems have become the dominant way in the past 30 or so years, but Type systems are not the only way.
For example, lets look at genetics. Genetics are based on the lineage of reproduction & mutations. The genetics of each organism in the lineage tree is essentially information. This information can be combined with another organism (sexual reproduction) to create a new organism. Also, an organism's genetics change over the lifetime of the organism.
A Type system could model the lineage of each organism in the tree, however it does not seem beneficial to model it in such a way from an abstract point of view. There may be practical reasons to model genetic lineage with types, but I can't think of any. My main reason is types ultimately reduce the resolution of the genetic information.
I feel like Type systems are akin to imposing a bureaucracy on individuals.
I appreciate this point of view. My perspective is absolutely that types are just one form of analysis and I don't mean to suggest that they should edge out others.
On the other hand, I think there genuinely is a kind of universality to types which cause them to (a) be as popular as they are and (b) apply in many (if not most, if not all) domains.
The essential core of this is that types/logic/category theory seem to be making significant headway at paving a new foundation of mathematics via MLTT/intuitionism/CT. These are dramatically general frameworks for creating structures and theories and providing a space for them to "hang together" in the obviously correct ways.
The generality and breadth of such a program is unbelievable! I won't try to convince anyone of its universality if they don't want to accept it—but I will suggest that the richness of MLTT/Intuitionism/Category Theory is sufficient to "probably" capture what you're interested in.
The cost is usually complexity. You could, for instance, "type" someone as their total genetic code. You could even type them as the union of every cell and the genetic code active in that cell. This is obviously incredibly, perhaps uselessly complex. But it's a great start. Then if you have quotients (which nobody has quite built into a type theory yet) you just start cutting down that complexity until you end up with whatever level of granularity you decide is correct.
Thank you for pointing me in the direction of MLTT/intuitionism/CT. I have a lot of good processing ahead of me.
One more thought about types. Stereotypes are a usage of types in our thinking. Stereotypes are a relatively low resolution (and low information load) way of defining a person. Stereotypes are a type system to model people.
Type systems seem to be brittle when it comes to increasing/decreasing resolution. It seems like type systems need to become more elaborate to account for these different resolution scopes that combine to ultimately make a concept. Just like imposing a type on an individual, one needs to account for the many nuances of that person. These nuances are sometimes & sometimes not applicable to other people with similar nuances.
One way to look at this is that you have types which classify a structure/theory. In some sense, it works like this—you have generators which allow you to inductively define a large set of "things", then you have laws which cut those things down.
For instance, the theory of monoids gives rise to the generators
zero : AMonoid
+ : AMonoid -> AMonoid -> AMonoid
satisfying the laws
zero + a = a
a + zero = a
a + (b + c) = (a + b) + c
Types can be refined and combined in principled ways by glomming the generators and laws together. Ultimately, what you're looking for is a notion of the set generated by all of the generators satisfying all of the laws plus any "coherence" laws which help to define what happens when two laws interact.
Unfortunately, nobody is very good at this today. It's a goal to be able to automatically achieve the above system in such a way that isn't O(n^2) effort to encode.
This notion of dynamically typed languages being a unityped static type system is how a static type system models a dynamic type system. If anything, it shows that dynamic type systems have nuance that can only be modeled as a "unitype" in a static type system, thereby exposing limits to static typing. The "unitype" also shows that types are orthogonal & incidental to solving the real problem. Types may or may not help the programmer, but types are not the direct solution.
I also object to Robert Harper's convoluted rationalization that dynamic type systems are less flexible because it goes against my practical experience. I'm not claiming that I'm the authority when it comes to programming languages. However, I gravitate toward dynamic languages in my career because I feel they offer me more flexibility & less incidental complexity than static languages.
That rebuttal is confused and unconvincing. It's easy, although clumsy and verbose, to write a very close equivalent of his "impossible to type check" code example in a static language. Define a sum type that ranges over the necessary values, define a few functions over that type that perform a case analysis corresponding to dynamic type checks, etc. That it's possible to do this is exactly the basis of Harper's argument that dynamic languages are subsumed within static languages.
Here's an concrete didactic example of the approach:
http://okmij.org/ftp/Scheme/scheme.ml
Static languages are not good dynamic languages (as currently designed), but they do subsume them.
This is not precisely about Tratt's response, but there was a great discussion on another Bob Harper post where Matthias Felleisen argued that while dynamic languages are semantically unityped, at the level of pragmatics (in the linguistic sense) they allow the programmer to freely mix various implicit type disciplines (http://existentialtype.wordpress.com/2014/04/21/bellman-conf...). The cost is of course that the programmer gets essentially no assistance in verifying that their implicit types are consistent.
There's no reason to believe that you can't freely mix implicit type disciplines in "statically typed" languages, either!
It's just (a) oftentimes you can actually reify those implicit schemes into actual types and it's often worth the cost to do so and (b) if your compiler depends upon a choice of type semantics in order to function and your implicit system is inconsistent with that selected type semantics then your analysis may not guarantee compilation!
But again: dynamic types are a mode of use of static types.
---
To be clear, this is the brunt of Bob's response in the linked thread anyway.
Interestingly the article also mentions optional type systems that recently became popular again like in Dart and Hack among other languages.
Optional typing provides a great middle ground between not being restricted by mandatory types when doing rapid iterations, yet getting the tooling benefits for core parts of your code base by using types to annotate signatures.
@tosh true this is so interesting article it also mention all type of system that became popular. but the most interesting are mandatory types by using annotate signatures.
> At the extreme end of the spectrum, the TCL language implicitly converts every type into a string
This isn't the full story. Since 1997, Tcl has used Tcl_Obj internally. These are called "dual-ported objects", where there are two values contained therein: a string value, to maintain Tcls logical model of "Everything Is A String" (EIAS), and a native value of the last-used-type. For example, if the object was last used as an integer, a native int value will be stored in the "internalRep". If the next use of this value is in an int context, this native internalRep value will be used. If one uses a value in an int fashion one call, then a float the next, then an int, then a float, then an int... you will incur what is called "shimmering", where the interalRep is recomputed back/forth. Shimmering is something to avoid where possible.
I don't like the article very much, especially the "Disadvantages of dynamic typing" section.
- The first point is about performance, which I doubt is the most fundamental difference between static and dynamic typing. The author even comments on whether performance truly matters, except in very low-level tasks, so why list it first?
- The real difference between the two systems, program correctness and early detection of errors, is hidden under the misleading title of "Debugging". It repeats the classic claim from dynamic typing proponents that "runtime type errors are rarely an issue", which is wrong in my experience (I've seen my share of ClassCastExceptions and NullPointerExceptions on production). Also, it advocates doing Unit Testing as a way to catch type errors, which I also find wrong. I'd rather focus on writing unit tests for other types of errors the compiler cannot help me catch.
Other parts also irk me:
- It lists "interactivity" as a strength of dynamic typing, when lots of languages with static typing have useful REPLs.
- The section on Built-in datatypes is baffling.
- Ditto for refactoring. Static typing for refactoring is a strength, not a weakness. About the only valid point here is that sometimes we want to temporarily break static checking of the whole program when testing a small section, but that probably can be handled by testing in isolation.
Steve Yegge, famously linked the Software Engineering with political axis. Interestingly he named people "Liberal" who prefer Dynamic languages over static.
I'm not saying it's not clunky, but all in all it's fairly pragmatic. That said, I'm a big Python fan as well. Of all the dynamic languages I work/worked with, it's the one that tries hardest to be less of a footgun, and it has a strong tradition of decent documentation (hear, hear, OCaml library developers...).
I'm not sure I understand. I use the maven shade plugin, so all there is at runtime is the JVM (system package) and the jar (built from libraries, but all of that's handled nicely with maven and its plugins), which can be fetched by http(s) from the repository and then just run (java -jar xyz.jar). There's no wrapping at the filesystem level but there doesn't need to be, because the classpath lets code load everything it needs from within that one jar file.
Shrug; I've found I spend less time debugging non-scala code when working in scala than I spend debugging non-python code when working in python. (When many popular python libraries go wrong, you need to know C).
His arguments for the advantages of statically typed language agree with mine. So, for my programming, I continue
to prefer static typing. Sorry 'bout that!
Sorry for going meta: does everyone also really enjoyed the formatting (spacing) and font choice of this article?
Its so, so good to read here (Win7/chrome) I'm thinking of copying it for my websites.
Justified, with different spacing between words seems really hard to me. The thin stems also make it hard to read the letters. Finally the column width is not adjustable by the browser (double tap on mobile, or resize window on desktop), which kills readability even more.
Smalltalk is a small, uniform object orientated language,...
"orientated"??
I hate to be a stickler, but you cannot say "object orientated" any more that you can say "the object was instantiatated", or "Xerox inventated Smalltalk".
"orientated" may be a perfectly cromulent word -- and may generally be a synonym for "oriented" -- but the phrase describing the programming paradigm is "object oriented" not "object orientated". Just as "functioning" is indisputably a good word and may be a rough synonym for "functional", but if you talk about about Haskell as a "functioning programming language", you may be correct in a sense, but it won't be as a statement about the programming paradigm it supports.
I don't dislike the word "orientated" (it is a real word), nor would I discourage it's use on either side of whatever pond. It's simply not correct to use it in the particular and very specific "object oriented" context. Much like the often mis-camel-cased "SmallTalk", it is incorrect.
Had Alan Kay coined the term "object orientated", I would use it without question.
None of those three links suggest a consensus against dynamically-typed languages. All of them feature highly-rated arguments in favor of such languages. How can you even begin to suggest a "consensus" from such a basis?
"in practice, run-time type errors in deployed programs are exceedingly rare [TW07]."
If we look at [TW07] they state that
"even very simple approaches to testing capture virtually all, if not all, the errors that a static type system would capture."
But provides no data or reference for that statement.
Another isue is that some references with data are based on small samples and possibly oudated:
"they [dynamc languages] lower development costs [Ous98]"
[Ous98] Compares time-to-implement and code-size for 8 different programs implemented in static and dynamic languages and shows that the dynamic languages are supperior. It is however not clear how much actual implementation is involved, so it may be the case that the difference is caused by diferences in available libraries at the time. In any case, the sample size is small and the article is old (1998) so it is not reasonable to make generalisations for programming in 2009 (or 20014).
[TW07] Laurence Tratt and Roel Wuyts. Dynamically typed languages. IEEE Software, 24(5):28–30, 2007.
[Ous98] John K. Ousterhout. Scripting: Higher-level programming for the 21st century. Computer, 31(3):23–30, 1998.