Static vs Dynamic « Primitive automaton

Internet is full with discussions about "Statically vs. Dynamically typed languages" (some of them: 1 2 3), and I want to add my own drop to the ocean.

When code is written, we want it to be correct, bug-free. Also if it is written quickly, that is a bonus. Both goals are hard to achieve simultaneously.

To make program correct we use many different techniques. If we are working on some algorithm, we might sketch it on the paper (alone or with a co-worker), go through some simple examples to see how our idea works. Than those examples turn into unit tests, and we might have some more generic tests, derived from "specifications". After the code is written, we give it to a teammate for review. We sometimes even write documentation, to explain ideas behind the lines of code. Also we add some logging here and there, so if in the future we encounter a problem, it's easier to find and understand.

With statically typed languages you start defining your data types and writing function type signatures (I'm thinking about how I write in Haskell). And then let types guide you through development.
With dynamically typed languages you start defining your data types, think about function type signatures, maybe write them down in the comments...

IMHO, in bigger projects statically typed language helps us to reduce silly errors.
We use static tools in dynamic languages, eg jshint for JavaScript, it catches silly variable name miss-spellings etc. Why not use static type-checker to help us catch more errors? The heart of the problem is that type systems of what-you-can-use-for-a-production-languages are often too restrictive.

For example we can do everything in simplest functional language, untyped lambda calculus, it's Turing complete and dynamic. But if we add the simplest type system to the language turning it into simply typed lambda calculus (abbreviated STLC), we lose Turing completeness, we can't type-check even basic a iteration, we need to either add special fix operator or recursive types with folds (read an introduction of this thesis) or catamorphisms (that's the fancy name).

Still STLC without polymorphic types is very restrictive. Even simple identity function

$\operatorname{id} = \lambda x . x$

cannot be type checked, we must give some hard type to the argument (and the result):

$\begin{aligned} \operatorname{id}_{\operatorname{int}} : \operatorname{int} \rightarrow \operatorname{int} & = \lambda x . x \quad \text{or} \\ \operatorname{id}_{\operatorname{string}} : \operatorname{string} \rightarrow \operatorname{string} & = \lambda x . x \end{aligned}$

This might feel really stupid, but think about [C](http://en.wikipedia.org/wiki/C_programming_language)( (without macros).

We can extend our type-system further, adding polymorphic types, just a bit ending to Hindley-Milner type system, or to the corner of lambda cube getting System F. Than we can write our useful identity function:

$\operatorname{id} : \forall\alpha.\alpha \to \alpha = \Lambda\alpha. \lambda x.x$

Hindley-Milner is in the heart of Haskell and ML, but we can extend the type systems. For example RankNTypes makes Haskell type system more like System F. There are also many others type-system extensions in GHC. And there are even some dependent type stuff for Haskell, but there are better alternatives if you want do that, like Agda or Idris.

Let's go through example. Now we have two extremes, in dynamic language, say JavaScript:

function first(arr) {
  return arr[0];
}

And in type dependent, static Coq (I prefer tactic based definition, because I seldom get it right with refine):

Definition first (A : Type) (l : list A) (H: l <> nil) : A.
  destruct l as [|x rest]. 
  (* l == nil *)
  exfalso. auto.
  (* l == x :: rest). *)
  exact x. Defined.

Haskell is somewhere in between:

first :: [a] -> a
first (x:_) = x

Coq's version will not permit you to apply first on a list, without a proof that the list is non-empty. Haskell will fail at run-time (with Non-exhaustive patterns in function first). We can make the error message better:

first :: [a] -> a
first (x:_) = x
first _     = error "`first` called with non-empty list"

BTW. Coq extraction mechanism is clever enough and will give similar Haskell output, with

Extraction Language Haskell.
Extraction Inline False_rect.
Extract Inductive list => "[]" [ "[]"  "(:)" ].
Extraction first.

we get

first :: ([] a1) -> a1
first l =
  case l of {
   [] -> Prelude.error "absurd case";
   (:) x rest -> x}

What will happen in JavaScript? If we pass an empty array, we get undefined back. We also get undefined, if we evaluate first(1). That behavior might be ok, or maybe we want to raise an error there. After adding explicit checks the code aren't elegant anymore:

function assert(exp, msg) {
  if (!exp) {
    throw new Error(msg);
  }
}

function first(arr) {
  assert(Array.isArray(arr), "arr must be an array");
  assert(arr.length !== 0, "arr must be non-empty array");
  return arr[0];
}

Dynamic languages are different, for example Python version

def first(l):
  return l[0]

will raise error if l is an empty list, or l doesn't behave like a list (effect of duck-typing).

In essence, the problem is that, if it walks like a duck and quacks like a duck, it could be a dragon doing a duck impersonation. One may not always want to let dragons into a pond, even if they can impersonate a duck.

Proponents of duck typing, such as Guido van Rossum, argue that the issue is handled by testing, and the necessary knowledge of the codebase required to maintain it.

And the latter one, necessary knowledge, is very hard to maintain or gather. Especially in large projects. Types can help you. Also you still want to do some asserts (even in Python, there is assert statement!) to make reasons of failing tests more clear.

In conclusion, with very sophisticated type system, you can express many contracts (pre- and post-conditions) using types. But convincing the type-checker may be tedious and time-consuming, so you may go for a run-time check. I would like softly typed language (I would prefer term quasistatic, like quasistatic processes in thermodynamics).

The key idea underlying soft typing is that a static type checker need not reject programs that contain potential type errors. Instead, the type checker can insert explicit run-time checks around “suspect” arguments of primitive operations, converting dynamically typed programs into statically type-correct form.

I have also written little JavaScript library to help with most common run-time checks in JavaScript: typify. It's not done, but already usable.

Static vs Dynamic

Comments