<p>The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of &quot;type system&quot; given on the page before:</p>
<blockquote>
<p><em>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.</em></p>
</blockquote>
<p>Note how aspects like &quot;syntactic method&quot; and &quot;classifying phrases&quot; mean that it applies to &quot;source&quot; programs, i.e., inherently is a static notion. Moreover, in actual type theory, programs that do not &quot;type-check&quot; are not even considered programs. The type system <em>defines</em> the set of well-formed programs. Something that's ill-typed has no meaning.</p>
<p>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 &quot;type&quot; 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 &quot;type system&quot; that would encompass &quot;dynamic typing&quot; without bordering on technically meaningless.</p>
<p>So from that technical point of view, a dynamic language is <em>untyped</em>, 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 &quot;tags&quot;.</p>

CC BY-SA 4.0
2020-06-27T12:29:57.273Z
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.
Martin Berger
CC BY-SA 4.0
2020-06-27T16:44:03.830Z
@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?
Andreas Rossberg
CC BY-SA 4.0
2020-06-28T11:52:49.057Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-06-28T14:17:40.110Z
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. https://lispcookbook.github.io/cl-cookbook/type.html)
Stefan
CC BY-SA 4.0
2020-07-04T11:18:12.630Z
@AndreasRossberg I'm afraid I can't agree with _" programs that               
do not "type-check" are not even considered programs."_ Type theory is a research methodology and practise for finding and expressing
structure in untyped $\lambda$-calculus.  You see this not just in
$\lambda$-calculus' historical emergence, but in most core theorems you
prove about a type theory (e.g.  type-soundness, subject reduction,
type-erasure): they relate typed and untyped programs. How would
you even formulate type-soundness without a more basic notion of
untyped computation?
Martin Berger
CC BY-SA 4.0
2020-07-04T11:26:34.617Z
@AndreasRossberg Yes, you can see $n+1$ stages as $n$ completely unconnected PLs with a
a binary compile-time / run-time distinction. But that lets you loose
sight of _how stages relate_, e.g.  the MetaML family of languages has
a single typing system that guarantees type soundess for all future
stages (this has advantages and disadvantage), but other languages
(e.g. Template Haskell don't do this).  You also loose the ability to
see the full all-stages computation as a single unified whole. (Part 1/2)
Martin Berger
CC BY-SA 4.0
2020-07-04T11:26:44.380Z
In
staged typing (like Template Haskell) your all-stages computation can
actually go wrong mid-compute, similar to languages like Python.
Finally, an ASTs in stage $i$, representing stage $i+1$ programs, are
in some sense tagged with sufficient type information in a way that is
not unline what you do do (or could do) with run-time typing. (Part 2/2)
Martin Berger
CC BY-SA 4.0
2020-07-04T11:28:49.700Z
In my experience, all substantial industrial computation has more than two stages, and the binary CT/RT distinction you find in TAPL is a nice simplification that helps beginners, but at at the same time is misleading in 2020. Any modern work on types makes more sense in the context of $n$-stage programming.
Martin Berger
CC BY-SA 4.0
2020-07-04T15:59:06.860Z
@AndreasRossberg It is possible  to add enough tags to programs, so that at run-time,  you capture the  the essence of a corresponding static typing system, see e.g. D. Vytiniotis, S. Peyton Jones, J. P. Magalhaes, _[Equality Proofs and Deferred Type Errors: A Compiler Pearl](https://www.microsoft.com/en-us/research/uploads/prod/2020/02/deferred-icfp12.pdf)_.  Related, see a lot of work on combining static and dynamic typing, e.g. TypeScript.
Martin Berger
CC BY-SA 4.0
2020-07-09T08:53:16.577Z
@MartinBerger, I'm not an expert on staged programming, so I suppose you're right. Though "all substantial industrial computation has more than two stages" does not match my experience. As for tags, in principle they can do quite a bit, but there are basic things they can't express, e.g. global properties like linearity. I'm aware of all the work on gradual typing etc, but it's coercions not tags. I wouldn't call out TypeScript, since it's fundamentally unsound by design, so doesn't provide real static _typing_ (research dialects like SafeTypeScript notwithstanding).
Andreas Rossberg
CC BY-SA 4.0
2020-07-09T09:07:30.477Z
@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.
Andreas Rossberg
CC BY-SA 4.0
2020-07-10T21:13:36.903Z
@AndreasRossberg How do you do typing a la Curry without untyped programs? Indeed, the
very concept of type inference is meaningless without untyped
programs. Not all type soundness can be proven while staying within
typable programs, for example some behavioural typing systems have
well-typed terms that reduces to non-typable intermediate terms before converging
to a typable value.  (1/3)
Martin Berger
CC BY-SA 4.0
2020-07-10T21:13:49.683Z
The first paper to introduce type-classes (S.
Kaes' _Parametric overloading in polymorphic programming languages_)                           
gives a system a la Curry, and hence starts from untyped                                       
$\lambda$-calculus. Same with _How to make ad-hoc polymorphism less ad                         
hoc_ by Wadler/Blott.  Linearity is a _dynamic property_ of resources in runs of a                          
computation. Typing systems enforcing linearity, are a syntactic                               
approximation to that dynamic property.  (2/3)
Martin Berger
CC BY-SA 4.0
2020-07-10T21:18:13.463Z
I agree that properties like linearity are not captured with immutable run-time tags, you need something more sophisticated, like  reference counters. (3/3)
Martin Berger
CC BY-SA 4.0
2020-07-11T10:54:29.913Z
@MartinBerger, aren't you conflating "untyped" with "unannotated"? An implicitly typed term in a Curry-style calculus is not untyped. AFAIAA, one motivation for only including well-typed terms is to avoid semantic models with junk elements. This is particularly inherent in mathematical type theory in the Martin-Löf sense, being a computational logic. For example, the HoTT book explicitly notes that "in type theory we cannot talk about an element _“a”_ in isolation: every element _by its very nature_ is an element of some type" (p.18).
Andreas Rossberg
CC BY-SA 4.0
2020-07-11T10:59:02.310Z
@MartinBerger, reference counting is an implementation technique, but in a semantics I believe it is insufficient to ensure linearity, unless we are able to impose some global _static_ well-formedness constraints on the overall program and state. Otherwise, what prevents forming a program/state containing an incorrect reference count and running it?
Andreas Rossberg
CC BY-SA 4.0
2020-08-03T13:00:11.490Z
@AndreasRossberg (1/2) I don't think the original question (and TAPL) understand
"type-theory" in the narrow sense of "model theory for HoTT".  Let's
distinguish: (A) **TT-CH** (for type-theory in the sense of the
Curry-Howard correspondence, a tool for structuring mathematical
proofs); (B) **TT-RW** (for type-theory in the real world, that
investigates types used in mainstream programming languages, from C++
to Scala to the SML to Haskell, to Java, type-script and beyond).  I
feel that nothing can be gained from not keeping those two shades of
meaning apart. (Continued.)
Martin Berger
CC BY-SA 4.0
2020-08-03T13:00:22.220Z
(2/2) In the sense of TT-RW I don't see the distinction between "untyped"
with "unannotated"? A program `17 * "Hello"` parses lexing and parsing
stages in idealised mainstream languages, but not type-inference. You
can see lexing and parsing as two very simple typing systems. I am not
sure what is gained by that.
Martin Berger
CC BY-SA 4.0
2020-08-03T13:08:36.937Z
@AndreasRossberg A resource is used linearly *in a run* if it is used exactly once in
that run.  A resource is linear *in a program* P if in all of P's runs
it is used linearly. A typing system is a tool for guaranteeing
linearity in a program P. If the typing system is decidable, it will have to
approximate linearity by Rice. Dynamically tracking linear resource
usage with a reference count can only report non-linear usage
immediately in the $n = 2$ case. The $n = 0$ non-linear usage can only
be flagged reliably at program termination.
Martin Berger
CC BY-SA 4.0
2020-08-04T08:35:10.143Z
@MartinBerger, much of modern PL type theory is derived from "TT-CH" foundations like System F or Martin-Löf. I believe that's what Pierce is referring to. Re untyped vs unannotated: I'm afraid I don't follow. The distinction occurs all over the literature, including TAPL. And it is pretty simple: a language is (generally speaking) untyped iff it allows `17 * "Hello"` to be executed. A typed language does not even define an operational semantics for it. Annotations don't occur in this example, so are unrelated.
Andreas Rossberg
CC BY-SA 4.0
2020-06-27T07:27:04.270Z
2020-06-27T07:27:04.270Z
Andreas Rossberg
<p>In the book <a href="https://en.wikipedia.org/wiki/Types_and_Programming_Languages" rel="nofollow noreferrer">&quot;Types and Programming Languages&quot;</a>, the author writes:</p>
<blockquote>
<p>The word &quot;static&quot; is sometimes added explicitly - we speak of a &quot;statically typed programming language&quot;, 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. <strong>Terms like &quot;dynamically typed&quot; are arguably misnomers and should probably be replaced by &quot;dynamically checked&quot;, but the usage is standard.</strong></p>
</blockquote>
<p>I am not sure if I understand this. Does the author mean that, in type theory, all programs are &quot;statically typed&quot;?</p>

<pl.programming-languages><type-theory><type-systems>
Why would the term "dynamically typed" be considered a misnomer?
Léo Vital
# Why would the term "dynamically typed" be considered a misnomer?

(Asked by: username_0 on 2020-06-27)

In the book ["Types and Programming Languages"](https://en.wikipedia.org/wiki/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"?

**Tags:** pl.programming-languages, type-theory, type-systems


---

## 1 answers

### Answer by username_1 on 2020-06-27. Score: 6 | Accepted answer

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".

> **Comments:**
> **username_2**: 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.  
> **username_1**: @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?  
> **username_3**: 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.  
> **username_4**: 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. https://lispcookbook.github.io/cl-cookbook/type.html)  
> **username_2**: @AndreasRossberg I'm afraid I can't agree with _" programs that                do not "type-check" are not even considered programs."_ Type theory is a research methodology and practise for finding and expressing structure in untyped $\lambda$-calculus.  You see this not just in $\lambda$-calculus' historical emergence, but in most core theorems you prove about a type theory (e.g.  type-soundness, subject reduction, type-erasure): they relate typed and untyped programs. How would you even formulate type-soundness without a more basic notion of untyped computation?  
> **username_2**: @AndreasRossberg Yes, you can see $n+1$ stages as $n$ completely unconnected PLs with a a binary compile-time / run-time distinction. But that lets you loose sight of _how stages relate_, e.g.  the MetaML family of languages has a single typing system that guarantees type soundess for all future stages (this has advantages and disadvantage), but other languages (e.g. Template Haskell don't do this).  You also loose the ability to see the full all-stages computation as a single unified whole. (Part 1/2)  
> **username_2**: In staged typing (like Template Haskell) your all-stages computation can actually go wrong mid-compute, similar to languages like Python. Finally, an ASTs in stage $i$, representing stage $i+1$ programs, are in some sense tagged with sufficient type information in a way that is not unline what you do do (or could do) with run-time typing. (Part 2/2)  
> **username_2**: In my experience, all substantial industrial computation has more than two stages, and the binary CT/RT distinction you find in TAPL is a nice simplification that helps beginners, but at at the same time is misleading in 2020. Any modern work on types makes more sense in the context of $n$-stage programming.  
> **username_2**: @AndreasRossberg It is possible  to add enough tags to programs, so that at run-time,  you capture the  the essence of a corresponding static typing system, see e.g. D. Vytiniotis, S. Peyton Jones, J. P. Magalhaes, _[Equality Proofs and Deferred Type Errors: A Compiler Pearl](https://www.microsoft.com/en-us/research/uploads/prod/2020/02/deferred-icfp12.pdf)_.  Related, see a lot of work on combining static and dynamic typing, e.g. TypeScript.  
> **username_1**: @MartinBerger, I'm not an expert on staged programming, so I suppose you're right. Though "all substantial industrial computation has more than two stages" does not match my experience. As for tags, in principle they can do quite a bit, but there are basic things they can't express, e.g. global properties like linearity. I'm aware of all the work on gradual typing etc, but it's coercions not tags. I wouldn't call out TypeScript, since it's fundamentally unsound by design, so doesn't provide real static _typing_ (research dialects like SafeTypeScript notwithstanding).  
> **username_1**: @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.  
> **username_2**: @AndreasRossberg How do you do typing a la Curry without untyped programs? Indeed, the very concept of type inference is meaningless without untyped programs. Not all type soundness can be proven while staying within typable programs, for example some behavioural typing systems have well-typed terms that reduces to non-typable intermediate terms before converging to a typable value.  (1/3)  
> **username_2**: The first paper to introduce type-classes (S. Kaes' _Parametric overloading in polymorphic programming languages_)                            gives a system a la Curry, and hence starts from untyped                                        $\lambda$-calculus. Same with _How to make ad-hoc polymorphism less ad                          hoc_ by Wadler/Blott.  Linearity is a _dynamic property_ of resources in runs of a                           computation. Typing systems enforcing linearity, are a syntactic                                approximation to that dynamic property.  (2/3)  
> **username_2**: I agree that properties like linearity are not captured with immutable run-time tags, you need something more sophisticated, like  reference counters. (3/3)  
> **username_1**: @MartinBerger, aren't you conflating "untyped" with "unannotated"? An implicitly typed term in a Curry-style calculus is not untyped. AFAIAA, one motivation for only including well-typed terms is to avoid semantic models with junk elements. This is particularly inherent in mathematical type theory in the Martin-Löf sense, being a computational logic. For example, the HoTT book explicitly notes that "in type theory we cannot talk about an element _“a”_ in isolation: every element _by its very nature_ is an element of some type" (p.18).  
> **username_1**: @MartinBerger, reference counting is an implementation technique, but in a semantics I believe it is insufficient to ensure linearity, unless we are able to impose some global _static_ well-formedness constraints on the overall program and state. Otherwise, what prevents forming a program/state containing an incorrect reference count and running it?  
> **username_2**: @AndreasRossberg (1/2) I don't think the original question (and TAPL) understand "type-theory" in the narrow sense of "model theory for HoTT".  Let's distinguish: (A) **TT-CH** (for type-theory in the sense of the Curry-Howard correspondence, a tool for structuring mathematical proofs); (B) **TT-RW** (for type-theory in the real world, that investigates types used in mainstream programming languages, from C++ to Scala to the SML to Haskell, to Java, type-script and beyond).  I feel that nothing can be gained from not keeping those two shades of meaning apart. (Continued.)  
> **username_2**: (2/2) In the sense of TT-RW I don't see the distinction between "untyped" with "unannotated"? A program `17 * "Hello"` parses lexing and parsing stages in idealised mainstream languages, but not type-inference. You can see lexing and parsing as two very simple typing systems. I am not sure what is gained by that.  
> **username_2**: @AndreasRossberg A resource is used linearly *in a run* if it is used exactly once in that run.  A resource is linear *in a program* P if in all of P's runs it is used linearly. A typing system is a tool for guaranteeing linearity in a program P. If the typing system is decidable, it will have to approximate linearity by Rice. Dynamically tracking linear resource usage with a reference count can only report non-linear usage immediately in the $n = 2$ case. The $n = 0$ non-linear usage can only be flagged reliably at program termination.  
> **username_1**: @MartinBerger, much of modern PL type theory is derived from "TT-CH" foundations like System F or Martin-Löf. I believe that's what Pierce is referring to. Re untyped vs unannotated: I'm afraid I don't follow. The distinction occurs all over the literature, including TAPL. And it is pretty simple: a language is (generally speaking) untyped iff it allows `17 * "Hello"` to be executed. A typed language does not even define an operational semantics for it. Annotations don't occur in this example, so are unrelated.  

---

