<p>There seem to be two conflicting views regarding the status of &quot;type systems&quot; used in dynamically typed languages:</p>
<ol>
<li><p>That dynamically typed languages are actually just <a href="https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages" rel="noreferrer">unityped static languages</a>. From what I can tell, the majority of type theory literature for programming languages (e.g. <a href="https://www.cis.upenn.edu/%7Ebcpierce/tapl" rel="noreferrer">Types and Programming Languages</a>) focuses only on statically typed languages, where by definition type checking is performed at compile-time. From this viewpoint, it seems reasonable to treat dynamically typed languages as being unityped.</p>
</li>
<li><p>On the other hand, the runtime engines of popular scripting languages like Python and JavaScript check the types of expressions during the program's execution, and raise an exception if there are any type errors. This feature seems to be <a href="https://tratt.net/laurie/research/pubs/html/tratt__dynamically_typed_languages" rel="noreferrer">common in dynamically typed languages</a>, and is colloquially referred to as &quot;strong typing&quot; (although this term is <a href="https://stackoverflow.com/a/2351869">discouraged</a>). In the <a href="https://www.cis.upenn.edu/%7Ebcpierce/tapl" rel="noreferrer">literature</a>, it seems standard to refer to these runtime types as &quot;type tags&quot;.</p>
</li>
</ol>
<p>Even though dynamically typed languages don't have genuine type systems according to the definition in point #1, it seems like many ideas introduced in type theory (e.g. polymorphism, subtyping) are directly applicable to understanding how these dynamic languages behave at runtime. Conversely, it seems reasonable that we could run a statically typed language line-by-line (e.g. in an interpreter) and handle type checking in an identical way to the method described in point #2.</p>
<p>So, my specific questions are:</p>
<ol>
<li><p>How useful is type theory for understanding dynamically typed programming languages?</p>
</li>
<li><p>Are there any formal theorems showing a direct correspondence between &quot;static types&quot; and &quot;runtime type tags&quot;? Can we just <a href="https://github.com/JuliaLang/julia/issues/6113#issuecomment-37338130" rel="noreferrer">replace the word &quot;type&quot; with &quot;type tag&quot;, and perform the type checking at runtime instead of ahead-of-time</a>, and then think about the programming language in terms of static type theory? If so, are there any limitations to this approach, e.g. situations where the analogy between &quot;static types&quot; and &quot;runtime type tags&quot; is no longer valid?</p>
</li>
</ol>

<types><static-typing><dynamic-typing><type-systems>
To what extent is type theory relevant to dynamically typed languages?
CC BY-SA 4.0
2023-08-14T13:08:03.330Z
Welcome! This is an interesting question, but to keep it focused enough for our format I suggest narrowing it down to just (1.) and (2.) ─ your (3.) is quite open-ended by itself.
kaya3
CC BY-SA 4.0
2023-08-15T01:16:47.933Z
Unlike in Python, it's very rare to get a type error in JavaScript because of implicit type conversion. `"3" * 4` is `12` (instead of "3333"), `"9"**"2"` is `81`, and `"string" / [1, 2, 3]` is `NaN`. The only ways I can think of to get a type error in JS are trying to access a property of something that isn't an object, and trying to call something that isn't a function :D
Quack E. Duck
CC BY-SA 4.0
2023-08-17T14:12:08.813Z
Thank you for the thoughtful answers everyone! I've accepted @Alexis King's answer because disentangling the terminology (as well as introducing the linked paper) was the most helpful for me. But I really appreciate everyone's contributions :)
Caleb Thomas
<blockquote>
<ol>
<li>How useful is type theory for understanding dynamically typed programming languages?</li>
</ol>
</blockquote>
<p>First of all, a <em>type system</em> is mostly about defining rules.
Let's take for example the definition of <em>Type system</em> as given by <a href="https://en.wikipedia.org/wiki/Type_system" rel="nofollow noreferrer">Wikipedia</a>:</p>
<blockquote>
<p>In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every &quot;term&quot; (a word, phrase, or other set of symbols). [...] This checking can happen statically (at compile time), dynamically (at run time), or as a combination of both. Type systems have other purposes as well, such as expressing business rules, enabling certain compiler optimizations, allowing for multiple dispatch, and providing a form of documentation.</p>
</blockquote>
<p>Note that the correctness of your program depends on whether or not it respects the language rules; you can check them at runtime or statically or not at all. Of course, practically, it is important that properties about a program are checked or enforced. But you tend to find a mix of static and dynamic checking/dispatch in most languages when it comes to types.</p>
<p>That being said, type systems are <em>designed</em> to be more easily checked at runtime or ahead-of-time: some features are added or removed to make sure that a static type checking decision procedure is sound, terminating, etc. (type theory).</p>
<p>If you want the program to be dynamically typed then a lot of type theory that is related to static typing is not going to be useful for you (higher-kinded type systems etc.). If later you want to guarantee some properties of your program statically, you'll need data-flow analyses or something else entirely.</p>
<p>If you take for example Python, it define <em>types</em>, like integer and strings, and under which rules they operate. So to me, the language defines a type systems: you have to understand classes and subtyping relationships, you have to understand if and how a value from one type is going to be interpreted as another type, etc. And these are the rules of your language whether you decide to interpret or compile it.</p>
<p>But you cannot easily describe this systems with a formal type theory designed for statically-typed languages.</p>
<blockquote>
<ol start="2">
<li>Are there any formal theorems showing a direct correspondence between &quot;static types&quot; and &quot;runtime type tags&quot;?</li>
</ol>
</blockquote>
<p>I don't think so but also I think both terms are not comparable. To me <em>&quot;type tags&quot;</em> are just a particular approach used to perform type checking at runtime: for example, you can also allocate one memory region for integers and another arena for floats: type checking at runtime is then a matter of checking in which memory region the value belongs (might be silly, this is not the point).</p>
<p>If the question is: can we always check types at runtime instead of statically, I guess the answer is yes (embed the compiler in the runtime and then its done dynamically?)</p>
<blockquote>
<p>Can we just replace the word &quot;type&quot; with &quot;type tag&quot;, and perform the type checking at runtime instead of ahead-of-time  and then think about the programming language in terms of static type theory?</p>
</blockquote>
<p>This question is not very clear to me.</p>
<blockquote>
<p>If so, are there any limitations to this approach, e.g. situations where the analogy between &quot;static types&quot; and &quot;runtime type tags&quot; is no longer valid?</p>
</blockquote>
<p>As said above, &quot;static types&quot; does not make much sense to me, there are <em>types</em> that are checked <em>statically</em> or <em>dynamically</em>, and &quot;runtime type tags&quot; is one way of doing the check at runtime.</p>

CC BY-SA 4.0
2023-08-14T22:05:45.247Z
2023-08-14T22:18:00.833Z
2023-08-14T22:18:00.833Z
coredump
CC BY-SA 4.0
2023-08-14T22:44:04.807Z
I’m not entirely convinced this answers the question. Sure, formal type systems are about defining rules, but that is very vague, and they are really about defining very specific sorts of rules. I don’t think this answer really makes the case that the rules used to formally specify type systems are adequate for capturing Python’s notion of types. Additionally, you say that you think it’s always possible to check types at runtime by embedding the compiler, but I don’t think that answer is really in the spirit of the question.
Alexis King
<h1>You are talking about type systems, not type theory</h1>
<p>I think it is worth drawing a distinction between <em>type theory</em> and <em>the theory of type systems</em>. Yes, this nomenclature is confusing, and yes, I realize this may seem like a pedantic quibble to many people. But they really are quite different:</p>
<ul>
<li><p><a href="https://en.wikipedia.org/wiki/Type_theory" rel="noreferrer"><strong>Type theory</strong></a> is a branch of formal mathematical logic. It is a direct descendant of set theory, and although many working type theorists are computer scientists, many of them are also pure mathematicians and logicians.</p>
</li>
<li><p>The <strong>theory of type systems</strong>, usually shortened to just <strong>type systems</strong>, is a branch of computer science, and more specifically a branch of the theory of programming languages.</p>
</li>
</ul>
<p>Of course, there are many close relationships between these two disciplines. They use similar notation, and they sometimes study similar things. Metatheoretical tools developed in type theory have been applied in the study of type systems and vice versa. However, type systems did not <em>originate</em> in type theory; to quote <a href="https://twitter.com/hillelogram/status/1301350242042998784" rel="noreferrer">Hillel Wayne</a>:</p>
<blockquote>
<p>I regularly see the claim that &quot;type theory invented type systems&quot;: that we have static typing because people tried to apply type theory to programming. This is untrue. The two concepts developed independently and were unified much later.</p>
</blockquote>
<p>For more background, see <a href="https://dl.acm.org/doi/abs/10.1145/2661136.2661154" rel="noreferrer">In Search of Types</a> (<a href="https://www.humprog.org/%7Estephen/papers/kell14in-author-version.pdf" rel="noreferrer">pdf</a>).</p>
<h1>The formal theory of type systems is a set of models</h1>
<p>The formal study of type systems rarely involves studying “real” programming languages. Instead, it studies simplified “model languages” and simpler languages used as compiler intermediate representations. The aphorism “all models are wrong, some are useful” largely applies here: most of these models are tools of thought that we value because they provide some insight or predictive power.</p>
<p>Since type systems, formally, are models, it should come as no surprise that there are often several different legitimate models for the same phenomenon, and they offer different perspectives that can be useful for different things. Bob Harper’s somewhat tongue-in-cheek “unityping” perspective is correct in that it is a legitimate model of dynamically typed programming languages, and sometimes it is even a helpful one! But it is also quite far removed from the informal <em>mental models</em> used by most working programmers writing dynamically typed programming languages.</p>
<h2>Gradual typing provides another perspective</h2>
<p>The theory of gradual type systems provides a very different model from the “unityping” perspective, and I would argue it is much closer to programmers’ mental models. Gradually typed languages often work very hard to support dynamic typing idioms, which requires developing typing rules that capture the rules those idioms abide by.</p>
<p>Since these type systems are not always enforced, they definitely do not provide a perfect model of dynamically typed languages, but they do provide a very useful one.</p>
<h1>The formal theory of type systems mostly does not study purely runtime typechecking</h1>
<p>From the perspective of programming language theory, a “type system” is more or less fundamentally a static analysis. For this reason, the theoretical definition of what a “type system” is does not line up perfectly with the definition that would likely be used by the working programmer:</p>
<ul>
<li><p>Many dynamically-typed languages have sophisticated runtime typechecking mechanisms, but a theoretical treatment would mostly consider these a part of the language’s operational semantics. Many of these systems would likely be more usefully modeled by the theory of <strong>contract systems</strong>.</p>
</li>
<li><p>Many programming language researchers would call many things “type systems” that programmers probably don’t think of as type systems. Many forms of static analysis can be usefully viewed in the framework of type systems, but they may not have all that much to do with programmers’ notion of types.</p>
</li>
</ul>
<p>It is important to underscore that this is not a failure of programming language theory to care about “real” systems, it’s just that researchers use a wide set of tools to model and analyze programming languages, and sometimes substantially different tools are needed to most usefully analyze things that programmers would consider very similar. For this reason, researchers often build models out of several pieces and prove that the different pieces are somehow consistent with each other.</p>
<p>For example, a language like Java would be understood by a programming language researcher as having both a static type system <em>and</em> a dynamic type system. The static type system could be modeled using formal typing rules, and the dynamic type system could be modeled using some form of operational semantics. The researcher could then prove statements about how these two systems cooperate in a consistent way.</p>
<p>For a working programmer, this level of formality is likely not helpful. But understanding the structures in an informal way can still be useful for understanding how programming languages really work. Ultimately, there is no one answer here, since again, many different models can be applied to the same programming language, but that’s all the more reason to learn several different perspectives and adopt whichever one happens to be most useful.</p>

CC BY-SA 4.0
2023-08-14T21:18:38.133Z
2023-08-15T15:12:02.217Z
2023-08-15T15:12:02.217Z
Alexis King
<blockquote>
<p>How useful is type theory for understanding dynamically typed programming languages?</p>
</blockquote>
<p>I would argue that type theory is important to the way that experienced programmers think about code, even when they are writing in a dynamically-typed language. For example, anyone who knows Python knows that this code is wrong:</p>
<pre class="lang-python prettyprint-override"><code>xs = [1, 2, 3, 4, 5]

for x in xs:
    print(x[0])
</code></pre>
<p>The reason we can see the code is wrong is because we know that <code>x</code> comes from <code>xs</code>, which is a list of integers, and therefore <code>x</code> must be an integer and has no <code>x[0]</code> subscript. But that is precisely the same reasoning that a type inference algorithm in a statically typed language would perform, and such algorithms are in the domain of type theory. So does it really matter, for our understanding of the language, whether that inference is done by the compiler or by our brains?</p>
<blockquote>
<p>[...] are there any limitations to this approach, e.g. situations where the analogy between &quot;static types&quot; and &quot;runtime type tags&quot; is no longer valid?</p>
</blockquote>
<p>Yes, there are many such situations. Consider the following code in Java:</p>
<pre class="lang-java prettyprint-override"><code>if(false) {
    Dog dog = new Cat();
}
</code></pre>
<p>This is a static type error, since <code>Cat</code> is not assignable to <code>Dog</code>. But because it occurs in unreachable code, it will never cause an error at runtime.</p>
<p>A similar example:</p>
<pre class="lang-java prettyprint-override"><code>Dog dog = true ? new Dog() : new Cat();
</code></pre>
<p>This is also a static type error, because the type of <code>a ? b : c</code> is whatever common type that both <code>b</code> and <code>c</code> can be converted to, e.g. <code>Object</code> in this case; and <code>Object</code> is not assignable to <code>Dog</code>. But runtime type checking would not raise an error, since the runtime type tag will be <code>Dog</code> whenever the expression is evaluated.</p>
<p>A different example:</p>
<pre class="lang-java prettyprint-override"><code>class Foo {
    static int foo(Object o) { return 1; }
    static int foo(Dog d) { return 2; }
}

int x = Foo.foo((Object) new Dog());
</code></pre>
<p>In Java the overloaded method <code>Foo.foo</code> is dispatched by the argument's static type, so this program will invoke <code>int foo(Object o)</code> and the result will be 1. But the cast <code>(Object) new Dog()</code> does not change the runtime type of the object, only the static type of the expression, so if the overload were dispatched by the argument's runtime type then <code>int foo(Dog d)</code> would be invoked and the result would be 2.</p>
<p>One more:</p>
<pre class="lang-java prettyprint-override"><code>List dogs = List.of(new Dog(), new Dog()); // bare List type
List&lt;Cat&gt; cats = (List&lt;Cat&gt;) dogs; // only a warning

Object dog = cats.get(0); // succeeds, returning a Dog
var cat = cats.get(0); // throws ClassCastException
</code></pre>
<p>This is an example of <a href="https://en.wikipedia.org/wiki/Heap_pollution" rel="noreferrer">heap pollution</a>, which can occur in Java due to bare generic types and type erasure. Here, the same expression <code>cats.get(0)</code> has a different meaning depending on the static type information provided by the surrounding context:</p>
<ul>
<li>When assigned to a variable of type <code>Object</code>, no runtime check is performed, because <code>Object</code> is the erased return type of <code>List.get</code>.</li>
<li>But when using a <code>var</code> declaration, the variable's type is inferred as the unerased return type of <code>List&lt;Cat&gt;.get</code>, which is <code>Cat</code>, and therefore a runtime check must be performed because the erased type is not assignable to the expected type.</li>
</ul>
<p>But the fact that <code>var cat = ...;</code> expects a <code>Cat</code>, and therefore that a check must be performed, can only be determined with respect to the static type of the expression <code>cats.get(0)</code>.</p>
<p>Now, none of this shows that type theory can't be applied to languages which only use runtime type tags. Rather, what it shows is that languages with static types and static checking may have semantics which can't be emulated using only runtime type tags and runtime checking.</p>

CC BY-SA 4.0
2023-08-14T14:01:28.967Z
2023-08-14T14:37:47.230Z
2023-08-14T14:37:47.230Z
kaya3
CC BY-SA 4.0
2023-08-14T14:15:03.840Z
What do you mean static types can't be emulated by runtime tags? What stop us interpret every check rule as an explicit assertion?
林子篆
CC BY-SA 4.0
2023-08-14T14:21:10.773Z
@林子篆 I gave three examples where that doesn't work. In the first example, the assertion is never checked so it has no opportunity to fail. In the second, the assertion passes despite the static type error. In the third, there is no type error, just different behaviour if static vs. runtime types are used.
kaya3
CC BY-SA 4.0
2023-08-14T14:28:27.417Z
In your first and second example, we still can lift them up to the proper place with a temporary variable, get assertion works. It's non-trivial, but exist a path. Beyond that, the error that will not happen is not important, static system do too much in this sense.

The third one you only check Java, and say no such system can do that, this is a problematic conclusion.
林子篆
CC BY-SA 4.0
2023-08-14T14:34:30.710Z
@林子篆 You cannot soundly move the unreachable expression `new Cat()` out of the block and evaluate it, because it can have side-effects which the program is not supposed to perform. But if you don't evaluate it then you won't see that its runtime type is `Cat` and not `Dog`. To determine that this is an error ─ whenever you determine that ─ you *must* find its type without evaluating it.
kaya3
CC BY-SA 4.0
2023-08-14T14:35:56.320Z
For the third example, you are misunderstanding something but I don't know what. I have not "only checked Java", I have presented an example *from* Java to show that a language can have semantics which require determining the static types of its expressions in order to determine their runtime behaviour.
kaya3
CC BY-SA 4.0
2023-08-14T14:45:30.603Z
Make sense, you recall my memory about the problem of unreachable combine side effect. I guess the root of my misreading is coming from "languages with static types and static checking may have semantics which can't be emulated using only runtime type tags and runtime checking". I read it more like type checking is not what runtime program can compute.
林子篆
CC BY-SA 4.0
2023-08-14T14:52:24.153Z
Runtime type checking is not enough, because it's only rely on current state, and context is a record for more, they indeed have different computation model. Now I understand it, maybe.
林子篆
CC BY-SA 4.0
2023-08-14T14:59:05.057Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/147888/discussion-between--and-kaya3).
林子篆
CC BY-SA 4.0
2023-08-15T07:49:27.887Z
"But runtime type checking would not raise an error, since the runtime type tag will be Dog whenever the expression is evaluated." - a dynamically typed language would have no use for giving the variable a manifest type, so the runtime type tag would be irrelevant anyway for a plain variable assignment (unless the type is inferred from the first assignment to a given name or something like that). Probably a better example would look like `(true ? new Dog() : new Cat()).bark()`.
Karl Knechtel
CC BY-SA 4.0
2023-08-15T12:17:36.063Z
@KarlKnechtel That's generally true if you are designing a language to be dynamically-typed in the first place, but the context here is whether you can convert static type checks to runtime type checks while preserving behaviour (except for the obvious behavioural difference that type errors would be raised at runtime instead of compile-time). In that case the variable's manifest type would have to correspond to a runtime check.
kaya3
<p>From my understanding, a dynamic language syntax might like: <span class="math-container">$x : \text{Expr}, y : \text{Expr} \vdash x + y : \text{Expr}$</span>. Therefore, one can write <code>1 + (lambda (x) x)</code>, which might not have reasonable result for most of us.</p>
<p>In static type system can use rule <span class="math-container">$x, y : \text{Int} \vdash x + y : \text{Int}$</span> as a check, and derives the result syntax's type, and prevents error from the beginning.</p>
<p>Dynamic setup has no information to check anything, so the idea is checking exactly before run it. Since primitive constants at most is countable, and operations is finite, we are able to rely on <strong>value's type</strong>.</p>
<p>Therefore, in this perspective, dynamic checking is delaying till need to use it. However, as <a href="https://langdev.stackexchange.com/a/2706/869">kaya3</a>'s answer, this way only supports expression that has no side effect.</p>
<p>Because side effect contains irreducible term like infinite loop, and  cannot be exchanged, thus code arrangement is not acceptable. For these code, get type by partial evaluation is required, and that need a state(aka at least pushdown automata is needed), and can touch original form of the syntax, and hence static. In this sense, there has semantic we cannot get from runtime tags.</p>
<hr />
<p>Beside the answer, type system might reduce too much, which make inconvenience. Hence, many different system are created to allow more reasonable use cases. Here is a type system way to do <strong>dynamic typing get/setter</strong> called strong update, naive case is:</p>
<pre class="lang-ocaml prettyprint-override"><code>let x = ref 1 (* x : ref int *)
x := true     (* x : ref bool *)
!x            (* !x : bool *)
</code></pre>
<p>This is interesting, setter will not care previous type, but just give it a new one, and getter accept the type in context. But conditional will involve more complicated problem:</p>
<pre class="lang-ocaml prettyprint-override"><code>if ... then
  x := false
else
  x := &quot;hello&quot;
(* what's x type here? *)
</code></pre>
<p>Introduce <strong>or</strong> type <code>(Bool | String) ref</code> might help, maybe others setup useful too, and this part should stop at here.</p>

CC BY-SA 4.0
2023-08-14T12:57:01.647Z
2023-08-14T19:54:06.033Z
2023-08-14T19:54:06.033Z
林子篆
# To what extent is type theory relevant to dynamically typed languages?
Posted by: username_0 on 2023-08-14
There seem to be two conflicting views regarding the status of "type systems" used in dynamically typed languages:

1. That dynamically typed languages are actually just [unityped static languages](https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages). From what I can tell, the majority of type theory literature for programming languages (e.g. [Types and Programming Languages](https://www.cis.upenn.edu/%7Ebcpierce/tapl)) focuses only on statically typed languages, where by definition type checking is performed at compile-time. From this viewpoint, it seems reasonable to treat dynamically typed languages as being unityped.
2. On the other hand, the runtime engines of popular scripting languages like Python and JavaScript check the types of expressions during the program's execution, and raise an exception if there are any type errors. This feature seems to be [common in dynamically typed languages](https://tratt.net/laurie/research/pubs/html/tratt__dynamically_typed_languages), and is colloquially referred to as "strong typing" (although this term is [discouraged](https://stackoverflow.com/a/2351869)). In the [literature](https://www.cis.upenn.edu/%7Ebcpierce/tapl), it seems standard to refer to these runtime types as "type tags".

Even though dynamically typed languages don't have genuine type systems according to the definition in point #1, it seems like many ideas introduced in type theory (e.g. polymorphism, subtyping) are directly applicable to understanding how these dynamic languages behave at runtime. Conversely, it seems reasonable that we could run a statically typed language line-by-line (e.g. in an interpreter) and handle type checking in an identical way to the method described in point #2.

So, my specific questions are:

1. How useful is type theory for understanding dynamically typed programming languages?
2. Are there any formal theorems showing a direct correspondence between "static types" and "runtime type tags"? Can we just [replace the word "type" with "type tag", and perform the type checking at runtime instead of ahead-of-time](https://github.com/JuliaLang/julia/issues/6113#issuecomment-37338130), and then think about the programming language in terms of static type theory? If so, are there any limitations to this approach, e.g. situations where the analogy between "static types" and "runtime type tags" is no longer valid?
**Tags:** types static-typing dynamic-typing type-systems
> **Comments:**
> **username_1**: Welcome! This is an interesting question, but to keep it focused enough for our format I suggest narrowing it down to just (1.) and (2.) ─ your (3.) is quite open-ended by itself.  
> **username_2**: Unlike in Python, it's very rare to get a type error in JavaScript because of implicit type conversion. `"3" * 4` is `12` (instead of "3333"), `"9"**"2"` is `81`, and `"string" / [1, 2, 3]` is `NaN`. The only ways I can think of to get a type error in JS are trying to access a property of something that isn't an object, and trying to call something that isn't a function :D  
> **username_0**: Thank you for the thoughtful answers everyone! I've accepted @Alexis King's answer because disentangling the terminology (as well as introducing the linked paper) was the most helpful for me. But I really appreciate everyone's contributions :)  
---
## 4 answers
### Answer by username_4 on 2023-08-14. Score: 17 | Accepted answer
# You are talking about type systems, not type theory

I think it is worth drawing a distinction between *type theory* and *the theory of type systems*. Yes, this nomenclature is confusing, and yes, I realize this may seem like a pedantic quibble to many people. But they really are quite different:

* [**Type theory**](https://en.wikipedia.org/wiki/Type_theory) is a branch of formal mathematical logic. It is a direct descendant of set theory, and although many working type theorists are computer scientists, many of them are also pure mathematicians and logicians.
* The **theory of type systems**, usually shortened to just **type systems**, is a branch of computer science, and more specifically a branch of the theory of programming languages.

Of course, there are many close relationships between these two disciplines. They use similar notation, and they sometimes study similar things. Metatheoretical tools developed in type theory have been applied in the study of type systems and vice versa. However, type systems did not *originate* in type theory; to quote [Hillel Wayne](https://twitter.com/hillelogram/status/1301350242042998784):

> I regularly see the claim that "type theory invented type systems": that we have static typing because people tried to apply type theory to programming. This is untrue. The two concepts developed independently and were unified much later.

For more background, see [In Search of Types](https://dl.acm.org/doi/abs/10.1145/2661136.2661154) ([pdf](https://www.humprog.org/%7Estephen/papers/kell14in-author-version.pdf)).

# The formal theory of type systems is a set of models

The formal study of type systems rarely involves studying “real” programming languages. Instead, it studies simplified “model languages” and simpler languages used as compiler intermediate representations. The aphorism “all models are wrong, some are useful” largely applies here: most of these models are tools of thought that we value because they provide some insight or predictive power.

Since type systems, formally, are models, it should come as no surprise that there are often several different legitimate models for the same phenomenon, and they offer different perspectives that can be useful for different things. Bob Harper’s somewhat tongue-in-cheek “unityping” perspective is correct in that it is a legitimate model of dynamically typed programming languages, and sometimes it is even a helpful one! But it is also quite far removed from the informal *mental models* used by most working programmers writing dynamically typed programming languages.

## Gradual typing provides another perspective

The theory of gradual type systems provides a very different model from the “unityping” perspective, and I would argue it is much closer to programmers’ mental models. Gradually typed languages often work very hard to support dynamic typing idioms, which requires developing typing rules that capture the rules those idioms abide by.

Since these type systems are not always enforced, they definitely do not provide a perfect model of dynamically typed languages, but they do provide a very useful one.

# The formal theory of type systems mostly does not study purely runtime typechecking

From the perspective of programming language theory, a “type system” is more or less fundamentally a static analysis. For this reason, the theoretical definition of what a “type system” is does not line up perfectly with the definition that would likely be used by the working programmer:

* Many dynamically-typed languages have sophisticated runtime typechecking mechanisms, but a theoretical treatment would mostly consider these a part of the language’s operational semantics. Many of these systems would likely be more usefully modeled by the theory of **contract systems**.
* Many programming language researchers would call many things “type systems” that programmers probably don’t think of as type systems. Many forms of static analysis can be usefully viewed in the framework of type systems, but they may not have all that much to do with programmers’ notion of types.

It is important to underscore that this is not a failure of programming language theory to care about “real” systems, it’s just that researchers use a wide set of tools to model and analyze programming languages, and sometimes substantially different tools are needed to most usefully analyze things that programmers would consider very similar. For this reason, researchers often build models out of several pieces and prove that the different pieces are somehow consistent with each other.

For example, a language like Java would be understood by a programming language researcher as having both a static type system *and* a dynamic type system. The static type system could be modeled using formal typing rules, and the dynamic type system could be modeled using some form of operational semantics. The researcher could then prove statements about how these two systems cooperate in a consistent way.

For a working programmer, this level of formality is likely not helpful. But understanding the structures in an informal way can still be useful for understanding how programming languages really work. Ultimately, there is no one answer here, since again, many different models can be applied to the same programming language, but that’s all the more reason to learn several different perspectives and adopt whichever one happens to be most useful.
---
### Answer by username_1 on 2023-08-14. Score: 9
How useful is type theory for understanding dynamically typed programming languages?

I would argue that type theory is important to the way that experienced programmers think about code, even when they are writing in a dynamically-typed language. For example, anyone who knows Python knows that this code is wrong:
xs = [1, 2, 3, 4, 5]

for x in xs:
    print(x[0])

The reason we can see the code is wrong is because we know that x comes from xs, which is a list of integers, and therefore x must be an integer and has no x[0] subscript. But that is precisely the same reasoning that a type inference algorithm in a statically typed language would perform, and such algorithms are in the domain of type theory. So does it really matter, for our understanding of the language, whether that inference is done by the compiler or by our brains?

[...] are there any limitations to this approach, e.g. situations where the analogy between "static types" and "runtime type tags" is no longer valid?

Yes, there are many such situations. Consider the following code in Java:
if(false) {
    Dog dog = new Cat();
}

This is a static type error, since Cat is not assignable to Dog. But because it occurs in unreachable code, it will never cause an error at runtime.
A similar example:
Dog dog = true ? new Dog() : new Cat();

This is also a static type error, because the type of a ? b : c is whatever common type that both b and c can be converted to, e.g. Object in this case; and Object is not assignable to Dog. But runtime type checking would not raise an error, since the runtime type tag will be Dog whenever the expression is evaluated.
A different example:
class Foo {
    static int foo(Object o) { return 1; }
    static int foo(Dog d) { return 2; }
}

int x = Foo.foo((Object) new Dog());

In Java the overloaded method Foo.foo is dispatched by the argument's static type, so this program will invoke int foo(Object o) and the result will be 1. But the cast (Object) new Dog() does not change the runtime type of the object, only the static type of the expression, so if the overload were dispatched by the argument's runtime type then int foo(Dog d) would be invoked and the result would be 2.
One more:
List dogs = List.of(new Dog(), new Dog()); // bare List type
List cats = (List) dogs; // only a warning

Object dog = cats.get(0); // succeeds, returning a Dog
var cat = cats.get(0); // throws ClassCastException

This is an example of heap pollution, which can occur in Java due to bare generic types and type erasure. Here, the same expression cats.get(0) has a different meaning depending on the static type information provided by the surrounding context:

When assigned to a variable of type Object, no runtime check is performed, because Object is the erased return type of List.get.
But when using a var declaration, the variable's type is inferred as the unerased return type of List.get, which is Cat, and therefore a runtime check must be performed because the erased type is not assignable to the expected type.

But the fact that var cat = ...; expects a Cat, and therefore that a check must be performed, can only be determined with respect to the static type of the expression cats.get(0).
Now, none of this shows that type theory can't be applied to languages which only use runtime type tags. Rather, what it shows is that languages with static types and static checking may have semantics which can't be emulated using only runtime type tags and runtime checking.
> **Comments:**
> **username_5** (2023-08-14): What do you mean static types can't be emulated by runtime tags? What stop us interpret every check rule as an explicit assertion?  
> **username_1** (2023-08-14): @林子篆 I gave three examples where that doesn't work. In the first example, the assertion is never checked so it has no opportunity to fail. In the second, the assertion passes despite the static type error. In the third, there is no type error, just different behaviour if static vs. runtime types are used.  
> **username_5** (2023-08-14): In your first and second example, we still can lift them up to the proper place with a temporary variable, get assertion works. It's non-trivial, but exist a path. Beyond that, the error that will not happen is not important, static system do too much in this sense.

The third one you only check Java, and say no such system can do that, this is a problematic conclusion.  
> **username_1** (2023-08-14): @林子篆 You cannot soundly move the unreachable expression `new Cat()` out of the block and evaluate it, because it can have side-effects which the program is not supposed to perform. But if you don't evaluate it then you won't see that its runtime type is `Cat` and not `Dog`. To determine that this is an error ─ whenever you determine that ─ you *must* find its type without evaluating it.  
> **username_1** (2023-08-14): For the third example, you are misunderstanding something but I don't know what. I have not "only checked Java", I have presented an example *from* Java to show that a language can have semantics which require determining the static types of its expressions in order to determine their runtime behaviour.  
> **username_5** (2023-08-14): Make sense, you recall my memory about the problem of unreachable combine side effect. I guess the root of my misreading is coming from "languages with static types and static checking may have semantics which can't be emulated using only runtime type tags and runtime checking". I read it more like type checking is not what runtime program can compute.  
> **username_5** (2023-08-14): Runtime type checking is not enough, because it's only rely on current state, and context is a record for more, they indeed have different computation model. Now I understand it, maybe.  
> **username_5** (2023-08-14): Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/147888/discussion-between--and-kaya3).  
> **username_6** (2023-08-15): "But runtime type checking would not raise an error, since the runtime type tag will be Dog whenever the expression is evaluated." - a dynamically typed language would have no use for giving the variable a manifest type, so the runtime type tag would be irrelevant anyway for a plain variable assignment (unless the type is inferred from the first assignment to a given name or something like that). Probably a better example would look like `(true ? new Dog() : new Cat()).bark()`.  
> **username_1** (2023-08-15): @KarlKnechtel That's generally true if you are designing a language to be dynamically-typed in the first place, but the context here is whether you can convert static type checks to runtime type checks while preserving behaviour (except for the obvious behavioural difference that type errors would be raised at runtime instead of compile-time). In that case the variable's manifest type would have to correspond to a runtime check.  
---
### Answer by username_5 on 2023-08-14. Score: 4
From my understanding, a dynamic language syntax might like: $x : \text{Expr}, y : \text{Expr} \vdash x + y : \text{Expr}$. Therefore, one can write 1 + (lambda (x) x), which might not have reasonable result for most of us.
In static type system can use rule $x, y : \text{Int} \vdash x + y : \text{Int}$ as a check, and derives the result syntax's type, and prevents error from the beginning.
Dynamic setup has no information to check anything, so the idea is checking exactly before run it. Since primitive constants at most is countable, and operations is finite, we are able to rely on value's type.
Therefore, in this perspective, dynamic checking is delaying till need to use it. However, as kaya3's answer, this way only supports expression that has no side effect.
Because side effect contains irreducible term like infinite loop, and  cannot be exchanged, thus code arrangement is not acceptable. For these code, get type by partial evaluation is required, and that need a state(aka at least pushdown automata is needed), and can touch original form of the syntax, and hence static. In this sense, there has semantic we cannot get from runtime tags.

Beside the answer, type system might reduce too much, which make inconvenience. Hence, many different system are created to allow more reasonable use cases. Here is a type system way to do dynamic typing get/setter called strong update, naive case is:
let x = ref 1 (* x : ref int *)
x := true     (* x : ref bool *)
!x            (* !x : bool *)

This is interesting, setter will not care previous type, but just give it a new one, and getter accept the type in context. But conditional will involve more complicated problem:
if ... then
  x := false
else
  x := "hello"
(* what's x type here? *)

Introduce or type (Bool | String) ref might help, maybe others setup useful too, and this part should stop at here.
---
### Answer by username_3 on 2023-08-14. Score: 2
> 1. How useful is type theory for understanding dynamically typed programming languages?

First of all, a *type system* is mostly about defining rules.
Let's take for example the definition of *Type system* as given by [Wikipedia](https://en.wikipedia.org/wiki/Type_system):

> In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). [...] This checking can happen statically (at compile time), dynamically (at run time), or as a combination of both. Type systems have other purposes as well, such as expressing business rules, enabling certain compiler optimizations, allowing for multiple dispatch, and providing a form of documentation.

Note that the correctness of your program depends on whether or not it respects the language rules; you can check them at runtime or statically or not at all. Of course, practically, it is important that properties about a program are checked or enforced. But you tend to find a mix of static and dynamic checking/dispatch in most languages when it comes to types.

That being said, type systems are *designed* to be more easily checked at runtime or ahead-of-time: some features are added or removed to make sure that a static type checking decision procedure is sound, terminating, etc. (type theory).

If you want the program to be dynamically typed then a lot of type theory that is related to static typing is not going to be useful for you (higher-kinded type systems etc.). If later you want to guarantee some properties of your program statically, you'll need data-flow analyses or something else entirely.

If you take for example Python, it define *types*, like integer and strings, and under which rules they operate. So to me, the language defines a type systems: you have to understand classes and subtyping relationships, you have to understand if and how a value from one type is going to be interpreted as another type, etc. And these are the rules of your language whether you decide to interpret or compile it.

But you cannot easily describe this systems with a formal type theory designed for statically-typed languages.

> 2. Are there any formal theorems showing a direct correspondence between "static types" and "runtime type tags"?

I don't think so but also I think both terms are not comparable. To me *"type tags"* are just a particular approach used to perform type checking at runtime: for example, you can also allocate one memory region for integers and another arena for floats: type checking at runtime is then a matter of checking in which memory region the value belongs (might be silly, this is not the point).

If the question is: can we always check types at runtime instead of statically, I guess the answer is yes (embed the compiler in the runtime and then its done dynamically?)

> Can we just replace the word "type" with "type tag", and perform the type checking at runtime instead of ahead-of-time and then think about the programming language in terms of static type theory?

This question is not very clear to me.

> If so, are there any limitations to this approach, e.g. situations where the analogy between "static types" and "runtime type tags" is no longer valid?

As said above, "static types" does not make much sense to me, there are *types* that are checked *statically* or *dynamically*, and "runtime type tags" is one way of doing the check at runtime.
> **Comments:**
> **username_4** (2023-08-14): I’m not entirely convinced this answers the question. Sure, formal type systems are about defining rules, but that is very vague, and they are really about defining very specific sorts of rules. I don’t think this answer really makes the case that the rules used to formally specify type systems are adequate for capturing Python’s notion of types. Additionally, you say that you think it’s always possible to check types at runtime by embedding the compiler, but I don’t think that answer is really in the spirit of the question.  
---
