3
$\begingroup$

In the book "Types and Programming Languages", the author writes:

The word "static" is sometimes added explicitly - we speak of a "statically typed programming language", for example - to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme, where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked", but the usage is standard.

I am not sure if I understand this. Does the author mean that, in type theory, all programs are "statically typed"?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before:

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

Note how aspects like "syntactic method" and "classifying phrases" mean that it applies to "source" programs, i.e., inherently is a static notion. Moreover, in actual type theory, programs that do not "type-check" are not even considered programs. The type system defines the set of well-formed programs. Something that's ill-typed has no meaning.

One could argue that this is the wrong definition. But it is shared by most researchers in the field and certainly by the ones working on type theory. It matches the notion of a "type" as established in mathematics and logic (lambda calculus, type theory). On the other hand, it would be difficult to come up with a sufficiently accurate definition of "type system" that would encompass "dynamic typing" without bordering on technically meaningless.

So from that technical point of view, a dynamic language is untyped, in the same way the untyped lambda calculus is (or equivalently, it has only one single type, such that every program is accepted as well-typed). Dynamic checks are not really on types but on the shape of values, which sometimes carry type-like "tags".

Improve this answer
$\endgroup$
20
  • 2
    $\begingroup$ Everything you say is correct -- under the 2-compute-phases assumption. But often you have more than 2 compute stages, e.g. in HPC or in web-programming, and what is 'run-time' to the $n-1$-stage is 'compile-time' to the $n+1$-stage. This is not really reflected in TAPL, and also usually ignored in the part of type-theory that comes from logic. $\endgroup$
    – Martin Berger
    Commented Jun 27, 2020 at 12:29
  • 1
    $\begingroup$ @MartinBerger, doesn't it carry over to staged programming as well? Each stage effectively is a DSL for generating programs of the next stage. And for each stage individually, this definition still applies. Or am I missing something? $\endgroup$
    – Andreas Rossberg
    Commented Jun 27, 2020 at 16:44
  • 2
    $\begingroup$ It's a fine quote, but I wish it said "absence or presence of certain program behaviors". The way it's written liveness properties of programs are excluded. $\endgroup$
    – Andrej Bauer
    Commented Jun 28, 2020 at 11:52
  • 1
    $\begingroup$ Note that people also talk about "type system" in the context of dynamically typed languages, even tho it means something a bit different in that context since it does not talk about a syntactic criterion on the source code (e.g. lispcookbook.github.io/cl-cookbook/type.html) $\endgroup$
    – Stefan
    Commented Jun 28, 2020 at 14:17
  • 1
    $\begingroup$ @MartinBerger, re "programs that do not "type-check" are not even considered programs": this is a technicality but still true in most type theories, where ill-typed terms (sometimes called pre-terms) simply have no meaning. For some more advanced type systems this actually is a necessity, since you wouldn't even be able to assign meaning, at least not without jumping through hoops (for a practical PL example, take Haskell with type classes). FWIW, standard preservation/progress proofs of type soundness do not depend on the existence of an untyped semantics. $\endgroup$
    – Andreas Rossberg
    Commented Jul 9, 2020 at 9:07

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.