In Practical Foundation of Programming Languages by Harper

There have been many attempts by advocates of dynamic typing to distinguish dynamic from static languages. It is useful to consider the supposed distinctions from the present viewpoint.

  1. Dynamic languages associate types with values, whereas static languages associate types to variables. Dynamic languages associate classes, not types, to values by tagging them with identifiers such as num and fun. This form of classification amounts to a use of recursive sum types within a statically typed language, and hence cannot be seen as a distinguishing feature of dynamic languages. Moreover, static languages assign types to expressions, not just variables. Because dynamic languages are just particular static languages (with a single type), the same can be said of dynamic languages.

  2. Dynamic languages check types at run-time, whereas static language check types at compile time. Dynamic languages are just as surely statically typed as static languages, albeit for a degenerate type system with only one type. As we have seen, dynamic languages do perform class checks at run-time, but so too do static languages that admit sum types. The difference is only the extent to which we must use classification: always in a dynamic language, only as necessary in a static language.

What do the first two sentences in the first part try to say:

  • What do dynamic languages associate with values: types or classes or both?

  • What is the significance of associating types or classes to values or variables? Do static languages associate types to variables but not to values? Do dynamic languages associate types or classes to variables besides values?



1 Answer 1


In those bullets, Harper is addressing common misconceptions about static versus dynamic typing. Each of those bullet points starts with a misconception, and then continues with Harper's clarification.

So, the first misconception is:

Dynamic languages associate types with values, whereas static languages associate types to variables.

Harper disagrees, and instead says that dynamic languages associate classes to values. This comes from a type-theoretic perspective, where it is useful to reserve the notion of a "type" to a particular form of static classification of expressions. In the textbook, Harper defends this perspective by demonstrating that "dynamic types" and "static types" can coexist, and in this way, the two concepts are orthogonal. In particular, there is a special static type which Harper calls dyn, and values of type dyn are given a tag at runtime which identifies their class, i.e. their "dynamic type". (By the way, it's worth mentioning that this tagging mechanism is exactly how dynamic types are implemented in modern languages.) In dynamically typed languages, it is often the case that the static types do not carry very much information, for example all expressions might actually have the static type dyn.

The interest in "values versus variables" comes from the "dynamic versus static" perspective on types. If we associate "types" with values, then we can only determine their "type" at runtime. But if we associate types with variables, then we can determine the type of the variable statically. Harper is just trying to point out that there doesn't need to be an issue of "this versus that": dynamic types and static types do not lie on the same spectrum. Simply put, from the perspective of type theory, "dynamic types" are not types.

To sum up, if we take a type-theoretic perspective and make a distinction between types and classes, then we can make this statement: all languages associate types with both variables and values. In fact, we can make an even stronger statement, which is this: all languages associate types with expressions. Variables and values are just two different forms of expressions.

  • $\begingroup$ Thanks. How shall I as a user tell whether a language is static typing or dynamic typing? Dynamic languages like Python call Harper's classes as "types", and that makes me not able to tell if they are dynamic or static typing. $\endgroup$
    – Tim
    Commented May 5, 2020 at 21:29
  • $\begingroup$ "How shall I as a user tell whether a language is static typing or dynamic typing?" – Two easy steps: Step #1: Provide a clear, precise, unambiguous, objective definition of the terms "static typing" and "dynamic typing". Step #2: check whether the language satisfies those definitions. Done. $\endgroup$ Commented May 6, 2020 at 21:35
  • $\begingroup$ @Tim: It's a matter of terminology. If you use Harper's definition of dynamic and static languages, you should use Harper's terminology. $\endgroup$
    – beroal
    Commented May 27, 2020 at 11:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.