The article suggests that static typing precludes duck typing. However, duck typing can work just fine at compile time. Duck typing simply means typing based on the ability to use particular methods or access particular properties. That just means the type system needs sufficient expressiveness to say that a function takes anything for which a particular method or property exists.
Haskell's typeclasses, for instance, support a form of duck typing. Go can do something similar with its interfaces.
Duck typing does not imply dynamic runtime typing; static duck typing seems just as useful.
Exactly the term I wanted, thanks! Just didn't manage to remember it.
Structural typing allows the creation of functions which only require their inputs to have the specific methods or properties needed to perform the given function, rather than an exact type. Effectively, this creates a minimal supertype for each function, such that the function can accept any subtype of that minimal supertype.
The common bias against structural typing is that there might be types with the same structure but subtly different semantics, e.g. coordinate systems. Same structural type, different semantic:
struct carthesian_coords { int x; int y; }
struct polar_coords { int r; int theta; }
Most of the structural typing systems I've seen count the names of fields as part of the type, not just the types of the fields. So, those two structs would have incompatible types in such a system.
Namely, "playing fast and loose with data representation"? That makes more sense, yeah. And now, it fits nicely with "pointer tricks" as something I can happily live without.
Mutation, on the other hand, I can easily see the arguments for either way; it represents a pretty large thing to give up in exchange for a more "obviously correct" programming environment. But pointer tricks have no place outside of low-level systems programming (OS kernels and language runtimes), and as little of that as possible to bootstrap something more comfortable.
I work on BITS (http://biosbits.org/), a project based on GRUB for doing BIOS testing. It has a pile of low-level C code to interface with hardware and system facilities, as well as other existing C interfaces like ACPICA; however, a while ago we ported the Python runtime, and since then we've ported more and more of the functionality to Python scripts.
Python doesn't have static typing, but it does handle memory management and object lifetimes automatically. It represents a good balance of high-level safety and comfort, acceptance by the target audience, and ease of porting to a freestanding environment with no OS support. I still wish I could find and eliminate more errors at compile time rather than only at runtime, but Python certainly manages to avoid the chainsaw-juggling feeling of programming in C.
It seems to me that much software can use a layered approach to get the best out of both systems. For example, in LedgerSMB, we use a highly engineered database on PostgreSQL, which means we can make the code "obviously correct" with regard to a number of invalid data bugs. We can then assign security to API operations declaratively using SQL roles. This makes the code obviously correct for certain classes of security issues and helps to mitigate other classes of security issues (for example SQL injection).
One of the key things to understand though is that "obviously correct" is always relative. There are, in fact, ways to circumvent these measures, and understanding where the problem areas lie. This means that most of the code may be "obviously correct" and some may be a bit less so. Knowing where that code is allows one to spend review time there.
The application above is written in Perl. However we are moving to Moose because it gives us a better ability to declare data constraints there.
I guess I'd call it "declaratively correct" instead of "obviously correct."
Nice set of qualities that make aspects of code obviously correct, but he forgot tests.
Like static typing, they are not perfect. They only catch certain classes of errors. But, when you have them, you have the assurance that the code behaves as it does in the test when the same conditions occur in production.
Disagree. Intuitively, the difference is that an "obviously correct" methodology changes the way you write code, whereas tests don't. Tests have to be run; the mere existence of a test doesn't mean your code is correct. But, crucially, the things a test checks don't generalize.
This isn't a perfect dividing line. If you add hooks for DI because you need to inject a mock, arguably that's changing the way you code (this is the schtick of TDD, after all!) Arguably, you have to "run the typechecker" in order to see if you actually have well typed code, and for a sufficiently powerful type checker this might be like running a program anyway. But hopefully the basic gist of the argument is there.
But, crucially, the things a test checks don't generalize.
I think this is the most important thing to note. When I say
Example test_fac1: (factorial 3) = 6.
Proof. reflexivity.
This is completely different from the statement
Theorem eq_fac : forall (n : nat),
fac n = prod 1 n
Tests are simply a mathematical proof of a relation on a specific subset of the domain and codomain of the function. Types, in the broad sense, are constrained proofs over the properties of all elements in the domain and codomain.
Types are useful -- they're perhaps the greatest success of formality in software engineering ever. However, they're not complete and completeness is hard. Types succeed because they provide a lot of benefit for very little pain (the constraints you discuss in your post). Your assertion is simply reinforced when we look at the other classes of correctness that we could guarantee. We could write fixpoint definitions for all functions which require structural recursion. We could push all side effects to typed lambda calculus sugar.
Fundamentally, we could prove our code correct. But that's a pain in the ass. And it still doesn't work. Tests complement proofs -- they ensure that our own conception of the definition fits our expectations. We could do all the work to formally prove our conjectures, but if our definitions were wrong the conclusions would be useless.
What I'm saying is that all of these things should work together -- and the result is a balancing act. We want additional guarantees that our programs are correct, but it requires us to program differently because only certain types of programs have the properties that we wish to exploit. The benefit is that we do have this additional information, so I agree that we should use it.
> [Tests] only catch certain classes of errors. But, when you have them, you have the assurance that the code behaves as it does in the test when the same conditions occur in production.
The trouble is, tests typically don't guarantee to catch an entire class of errors. Rather, each test guarantees to catch one specific case, and when you write your tests you try to cover a useful number of representative cases.
This is not to say that executable tests don't have their place, of course, but the plural of "unit test" is not "proof". On the other hand, if you can verify a certain property totally via your type system then executable tests for that property are unnecessary.
>What all of these “obviously correct” methodologies ask you do is to sacrifice varying degrees of expressiveness at their altar.
In the case of static types, this is simply untrue. Embedding dynamic types into static type systems is a triviality. With compiled code, there is generally a substantial speed up at runtime assocaited with a good static type scheme.
I think this is missing the point. On a practical level, most of these "obviously correct" methodologies have escape hatches: i.e. FFIs for memory safety. On a theoretical level, by embedding dynamic types in a statically typed language, you have a stratification where code written in the host typing is "clear of typing bugs", but code written in the embedded typing is less sound. You need to distinguish between these two layers.
The point made in the OP is that expressiveness is sacrificed by having these safety features. This is simply not the case with static typing, because of the ease with which dynamic typing is embedded in a static type system.
"code written in the embedded typing is less sound" - Well the point maybe is that static typing did not bring quite the safety some thought it did: it only promised that these functions must return, if they do return, a value of a given type. The ability to model dynamic typing inside static typing shows just how weak this guarantee can be. More generally, it show there is no expressiveness sacrifice.
I think the crux of the issue here is "triviality."
I claim that it is nontrivial to embed dynamic types in a statically typed language. Usually this is due to the need to add lots of explicit coercions in order to interface with all of the code is actually statically typed. I can embed a dynamically typed programming language in my statically typed language, with its own libraries, but that's hardly "trivial".
Difficulty matters. Otherwise I can claim that I can bypass memory safety by writing a simulator for x86 in a memory safe language, and, well, the code that runs might violate memory safety (in some alternate sense), and thus, there is no expressiveness sacrifice!
"lots of explicit coercions" - even without recourse to generics, the overhead tends to be small. Really, try it. There's no need to write intepreters, let alone architecture simulators.
I tend to think the attraction of dynamic typing is the ability to run incomplete or ill-typed programs. If we have type inference, there is no real advantage in terms of conciseness.
What do you mean? You can map each dynamically typed function/procedure onto a statically typed function/procedure that is used in the same way. I do not see how a translation could be cleaner and more structure preserving.
> CPython was never explicitly engineered for performance, whereas the JVM had decades of work poured into it.
* Often IO latency and throughput is such that fast CPU processing doesn't really matter. IO is the bottleneck and Python is often fast enough.
* Look @ speed and improvements in PyPy (keeping in mind their team size and budget) in just recent years vs JVM's man hours over the years. Just because there were decades of performance poured into it, doesn't make something proportionally better.
Interestingly enough, I was talking to Quora engineers about the problems they were facing scaling their website, and there was no doubt about it: CPU was one of the big problems. Yes, yes, I know, don't overengineer your systems in the beginning, but I really get the sense that if software needs to scale, it is going to need to scale in all dimensions, including CPU.
I'll note that the "JVM has had more hours poured into it" argument is meant to give PyPy the benefit of the doubt!
Quora's move from Python to Scala is a 'clear indicator' of the 'fact' that type safety is better? That's just a weak and clearly incomplete line of reasoning.
Haskell's typeclasses, for instance, support a form of duck typing. Go can do something similar with its interfaces.
Duck typing does not imply dynamic runtime typing; static duck typing seems just as useful.