blog

Robert Harper points out that dynamically typed languages are a subset of statically typed languages. To wit, we could handle J values in Haskell with something like:

data JData = JIntArr (Array CLLong)
           | JDoubleArr (Array CDouble)
           | JComplexArr (Array (Complex CDouble))
           | JBoolArr (Array CChar)
           | JString !ByteString

(+) :: JData -> JData -> JData
(JIntArr is) + (JDoubleArr xs) = JDoubleArr (fmap fromIntegral is + xs)
...

Functional programming tends not to emphasize this fact, though Haskell does something similar with its Integer type.

However, types in Haskell are not only classifications that refine acceptable inputs, they also serve a positive rôle as witnesses to a particular implementation^[1]—typeclasses. As an example, suppose we have written a function ncdf :: Double -> Double. Then the below runs a property test:

 > quickCheck $ \x -> ncdf x > 0 && ncdf x < 1
+++ OK, passed 100 tests.

Thus there are two aspects of types^[2] that get confused, particularly when talking about statically typed vs. dynamically typed languages.

Python's unitype, PyObject, underlies every value, but one can define methods on a per-type basis; for example, calling print on a number vs. a string entails different code being executed, different parts of the PyObject being inspected. Method definitions are added to the environment over the course of program evaluation, subject to control flow.

In this way, what Python calls types are truly dynamic—one could define a method or not depending on the CPU temperature. Witnesses are set out at runtime, quite different from the situation with typeclasses in Haskell.

My claim is that the vexations attributed to static types overwhelmingly arise from the positive rôle, that is, finding witnesses for typeclasses. There is little merit in failing at runtime rather than gating compilation (most type errors are irredeemable).

Confusion arising from typeclasses should not be taken as a strike against static typing. It is not obvious that dynamically typed languages like Python could do better—in Haskell, instances are not globally unique, muddling established approaches. Instances defined based on runtime control flow would only make this thornier!

[1] Gating acceptable inputs is negative, recessive abstraction. Witnesses are positive, expansive.

[2] Type variables enforce universality and actually have a negative (recessive) rôle. A function defined by typeclasses such as sum :: Num a => [a] -> a recalls universal quantification over a predicate but the typeclass brings in positive aspects (finding a witness/dispatching an implementation for (+)).