<p>The advantages of an expressive type system cannot be denied. The usual definition applies - how much valid behaviour a chosen system allows, while also preventing invalid behaviour.</p>
<p>In terms of &quot;expressiveness&quot; of type systems, i've come up with the follow (partial) hierarchy, where the intent is that each system allows more valid behaviour than the one before it. This is mostly based off the lambda cube. I'm also only considering &quot;strong&quot; type systems, so nothing like C's. Please also further note that this is not the only ordering of type systems - As per the lambda cube, any possible ordering would need to be inherently partial. In this case, I have tried to select type systems I have seen practically used by (somewhat) popular languages.</p>
<p>I am also excluding things like traits in this list, as they can be (mostly) trivially added to any of these in at least a limited way.</p>
<ul>
<li>No polymorphism, base types only : eg, STLC</li>
<li>Rank-1 : OCaml</li>
<li>Rank-2 : GHC Haskell w. -XRank2Types, MLF</li>
<li>System F : GHC Haskell w. -XRankNTypes</li>
<li>System Fω : Terms that depend on types, types that depend on types. GHC Core - one of the IRs of GHC Haskell.</li>
<li>MLTT[1] / CIC[2] : Full dependent types. Agda/Coq/Lean/Idris.</li>
<li>CTT[3] : Full dependent types, and higher inductive types. Cubical Agda is the only impl I am aware of.</li>
<li>Something even more expressive i'm not aware of?</li>
</ul>
<p>[1]: Martin-Löf Type Theory
[2]: Calculus of Inductive Constructions
[3]: Cubical type theory</p>
<p>My question is at what point has it been shown that the average user starts getting confused more often than not? While a stronger type system allows more valid behaviour, it also inevitably becomes more confusing - especially once you start to get into dependent type territory with Fω, so I wouldn't be surprised if this is that cutoff point.</p>
<p>Please note that I am not asking for personal opinions on the matter; if possible, any sort of quantitative evidence would be appreciated. I have tried various search engines to see if there is there is anything preexisting on the matter, but I have not found much, so I'm curious if anyone here has anything.</p>

<type-systems><type-theory><polymorphism><dependent-types>
How expressive of a type system is too expressive, for the average programmer?
CC BY-SA 4.0
2023-08-23T23:37:58.497Z
Judging from your hierarchy, it seems like a better term would be "expressivity" rather than "strength". I also don't see what this hierarchy has to do with "loopholes" ─ a language could have a type system in any of these categories, while also having (or not having) an escape hatch. It's also somewhat debatable whether your hierarchy really reflects type systems "prevent[ing] as many errors as possible"; for example any mistake possible to make in the simply-typed lambda calculus is also possible to make in a more expressive type system, if you just don't use the additional features.
kaya3
CC BY-SA 4.0
2023-08-23T23:46:10.877Z
The first paragraph seems to take "strong" in the conventional "strong typing" binary property sense, but the rest uses "strength" differently to mean comparable *degree* of complexity, expressivity, depth, or something else. I think it'd be clearer to tidy this up somehow with distinct terminology (although I'm not convinced that this *is* a total order either). For what it's worth, I don't believe that any such studies *have* been run, but in theory they could, so seeking that information is a fine question and I'd be interested in an answer to it.
Michael Homer
CC BY-SA 4.0
2023-08-24T00:43:13.120Z
@kaya3 Would a better wording perhaps be "Allowing as much as possible expressivity as possible within it's domain?" If so, please feel free to edit the question yourself, or I'll edit it when I have time.
blueberry
CC BY-SA 4.0
2023-08-24T00:43:55.930Z
@MichaelHomer In retrospect I agree. I'll edit the question as soon as I have some time to reword everything to not use "strong".
blueberry
CC BY-SA 4.0
2023-08-24T01:01:08.530Z
GHC Core, an important intermediate language used by the GHC Haskell compiler, essentially uses System Fω, AFAIK. Haskell itself, if you count extensions, *almost* has System Fω in the type system with its type families, but you there is no general-purpose type abstraction (`Λ`) and you can't straightforwardly fake it using type families.
David Young
CC BY-SA 4.0
2023-08-24T01:03:08.810Z
I agree with @MichaelHomer that there probably isn't a total order for expressiveness. See, for example, [the lambda cube](https://en.wikipedia.org/wiki/Lambda_cube). That is an ordering on expressiveness that is not a total order. For instance, λP and λ2 are incomparable in the lambda cube ordering
David Young
CC BY-SA 4.0
2023-08-24T02:20:04.360Z
@DavidYoung That's why i've presented at least one possible partial ordering here - I've tried to select the type systems that i've seen either practically used, or "inbetween" ones that are practically used. I've never seen a widely used language that uses either of λP or λ2, so I didn't include them. See your other comment for why I included Fω.
blueberry
CC BY-SA 4.0
2023-08-24T02:21:50.380Z
@DavidYoung I'll add GHC Core as an example for Fω, thank you.
blueberry
CC BY-SA 4.0
2023-08-24T09:07:41.480Z
Is the characterisation of OCaml correct? OCaml has objects and first-class modules, GADTs - not present for example in Standard ML.
Christian Lindig
CC BY-SA 4.0
2023-08-24T10:39:15.727Z
The "average programmer" does not use OCaml or Haskell, let alone Agda/Coq/Lean/Idris. The average programmer uses Python, JavaScript / TypeScript, Java, Kotlin, C++, C, etc. So the language examples you state are in contradiction with the question. The fact that most mainstream languages have type holes does not make them uninteresting for the question. Furthermore, as far as my limited understanding of type systems goes, there are things you can type in these mainstream languages, that you cannot in Haskell: this is not a one-dimensional hierarchy.
Jean-Armand Moroni
CC BY-SA 4.0
2023-08-24T22:56:22.483Z
@ChristianLindig While OCaml technically does have first class polymorphism (ie rank N) via the use of modules and records, I felt it more useful to only include the "standard" things an OCaml programmer would use, which is rank-1. (Also, GADTs and first class modules fall under the "traits" category above, ie they can be added to any of the systems). Don't worry, I'm not trying to mischaracterise OCaml; it's my day-to-day language ;)
blueberry
CC BY-SA 4.0
2023-08-25T14:23:55.740Z
You are missing out some orthogonal dimensions in typing, in particular the quantitative dimension (e.g. linear vs affine) and the parallelism dimension (e.g. session types).
Martin Berger
CC BY-SA 4.0
2023-08-25T14:29:14.850Z
There is a complementary dimension to your *what* type features are problematic, namely *when* do they start becoming problematic. To paraphrase a colleague: _types are like cocaine: you see the benefits immediately and you want more, but the problems only later_ ...
Martin Berger
CC BY-SA 4.0
2023-08-31T22:50:53.700Z
Judging from Go, many programmers consider enums and sum types too complex…
xigoi
<p>This is an interesting question, but I want to first break down the two big assumptions.</p>
<p>First, assuming the &quot;average&quot; programmer has some sort of type expressiveness limit is probably nonsensical. Otherwise, the answer seems to be that <em>every</em> type system is too expressive. The <a href="https://survey.stackoverflow.co/2022/#most-popular-technologies-language" rel="noreferrer">2022 Stack Overflow Developer Survey</a> indicates that over half of the top 10 languages have no static typing at all. The other half do not have very expressive type systems relative to your examples (except Typescript), and zero of them are sound. Additionally, the only research I could find into this mostly has to do with dynamic vs. static type systems (see <a href="https://softwareengineering.stackexchange.com/questions/10032/dynamically-vs-statically-typed-languages-studies">this thread</a>), which signals to me that there isn't much literature on the subject yet.</p>
<p>Another problem here is that &quot;moving up&quot; to higher order type systems, while technically more expressive, has quickly diminishing returns regarding practicality in a real program. Pierce's <a href="https://www.cis.upenn.edu/%7Ebcpierce/tapl/" rel="noreferrer">Types and Programming Languages</a> briefly discusses this, saying</p>
<blockquote>
<p>A natural question at this point is “Why stop at three levels of expressions?” Couldn’t we go on to introduce functions from kinds to kinds, application at the level of kinds, etc., add a fourth level to classify kind expressions
according to their functionality, and continue on in this way ad infinitum?
Such systems have been investigated by the pure type systems community [...]. For programming languages, however, three levels have proved sufficient.</p>
</blockquote>
<p>We can see this in modern programming languages. Haskell, for example, lowers to GHC Core, which is an augmented version of System F (it does not quite make it to F<span class="math-container">$_\omega$</span>). Simon Peyton Jones has a great paper on it, which you can read <a href="https://gitlab.haskell.org/ghc/ghc/-/blob/master/docs/core-spec/core-spec.pdf" rel="noreferrer">here</a>. OCaml, and other ML languages, use a restricted version of System F. The only languages that offer more expressive type systems are almost entirely restricted to the domain of proof assistants.</p>
<p>So, if we are looking at current languages, it seems that F<span class="math-container">$_\omega$</span> is pretty much the limit -- you don't hear a lot of people complaining that Haskell isn't expressive enough.</p>
<p>If you wanted to add more <em>real world</em> expressiveness to a type system, I would go about it by adding features, instead of adding another level of expression. Algebraic data types, type families, type classes, and GADTs, to name a few examples, can all be added to a system less powerful than F<span class="math-container">$_\omega$</span>. I would argue that these features increase real world expressiveness more than (for example) a 4 or 5 layer system ever would, and allow programmers to eliminate more classes of error, which I think is the real goal here.</p>

CC BY-SA 4.0
2023-08-24T04:08:38.603Z
2023-08-24T04:08:38.603Z
Luke LaBonte
CC BY-SA 4.0
2023-08-24T04:28:53.863Z
For what it's worth, if the limit is "the average dev doesn't want to even handle a static type system, let alone a complex one", then i'm willing to accept that. Please also be assured that by "limit" I don't mean a conceptual one; i'm sure almost all devs would be able to *understand* the more complex half of this hierarchy if given time to learn it, but it's more about whether they're *willing* to, in which case an answer of "any static system" is a perfectly valid answer.
blueberry
CC BY-SA 4.0
2023-08-24T08:58:45.573Z
The last paragraph is key. Having good base types, sums, products, ad-hoc and parametric polymorphism supported by syntax is more relevant than a theoretically more powerful system where everything is a lambda term (which is enough to study the expressiveness but not to build something).
Christian Lindig
CC BY-SA 4.0
2023-08-24T12:26:58.157Z
Welcome, and a great first answer! Totally agree about the last paragraph; for Typescript in particular, mapped and conditional types are excellent for expressing relations between types, so that if you want to change the design later you only have to change it in one place. And whlie it's technically outside of the type system, control-flow type narrowing is a feature which can make the type system more useful.
kaya3
CC BY-SA 4.0
2023-08-24T14:50:03.250Z
@blueberry I think anyone operating in a non-pure research environment would have to ask the question "what benefits can *only* be achieved by this type system, and what commercial value do they have compared to the retooling cost".
pjc50
CC BY-SA 4.0
2023-08-25T01:42:57.533Z
@pcj50 I would have hoped that was implicit in my wording above, but if it wasn't, I apologise for me not being clear.
blueberry
CC BY-SA 4.0
2023-08-25T01:43:17.530Z
I'm going to accept this, as the community seems to like it and it contains some good information.
blueberry
CC BY-SA 4.0
2023-08-28T02:15:41.917Z
"the average dev doesn't want to even handle a static type system, let alone a complex one" however, many devs prefer the benefits of static typing, and type inference is quite popular in newer languages, which gives the syntax of a dynamic language but the power of static typing
Seggan
CC BY-SA 4.0
2023-09-01T03:45:35.660Z
@Seggan To say that type inference is popular in newer languages is a bit odd; ML has been around since '83 with full program type inference, and variants of said are still quite popular today. I'd say it's more accurate that people are only realizing how nice it is recently, not that it wasn't possible.
blueberry
CC BY-SA 4.0
2023-09-01T12:33:53.143Z
I never said it wasn't *possible*. I said that just now it's beginning to drop up in the mainstream.
Seggan
<p>Luke LaBonte already gave an excellent answer. I just want to add some things:</p>
<blockquote>
<p>My question is at what point has it been shown that the average user starts getting confused more often than not?</p>
</blockquote>
<p>I think people are generally confused in these two cases:</p>
<ol>
<li>If the type system is introduced before you need it, and especially when it's not described using simple examples in your programming language. If I read articles about type systems that come from a functional programming perspective and that use some <a href="https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation">weird notation</a>, my eyes glaze over.</li>
<li>When something that looks natural in your programming language to write, but then the compiler/interpreter does something unexpected or throws an error.</li>
</ol>
<p>As an example of 1, introducing people to C++'s template system before they need it is a bad idea; they will probably dislike it and avoid it. However, if you tell them to write an implementation of a linked list of <code>int</code>s, and then ask them to make it work for <code>float</code>, <code>std::string</code> and ten other types, they will figure out that it would be really nice if that <code>int</code> could be replaced with some type variable, and then suddenly introducing the <code>template&lt;typename T&gt;</code> notation seems logical. And suddenly they understand generic types.</p>
<p>As for 2, consider someone know that you can create arrays of a given length like <code>std::array&lt;int, 10&gt;</code> in C++. But now they have to read some data with variable length. It's then very natural to write:</p>
<pre><code>std::size_t length;
std::cin &gt;&gt; length;
std::array&lt;int, length&gt; my_array;
</code></pre>
<p>However, that will not compile, because C++ only allows types to depend on compile time constants, not on runtime values. The programmer will think: &quot;why can't the compiler just do what I want?&quot; With &quot;what I want&quot; being the possibility of having dependent types.</p>
<blockquote>
<p>While a stronger type system allows more valid behaviour, it also inevitably becomes more confusing - especially once you start to get into dependent type territory with Fω, so I wouldn't be surprised if this is that cutoff point.</p>
</blockquote>
<p>I agree with Luke that there is no such cutoff point. Rather, I think a programmer will at some point come upon a situation where they would need something that is obvious at the moment, but would be considered an advanced type system feature. The programmer also doesn't need to understand type theory as you would teach it at a computer science course, they just need to understand it in terms of how to use their programming language to achieve it.</p>

CC BY-SA 4.0
2023-08-24T14:19:49.690Z
2023-08-24T19:24:29.220Z
2023-08-24T19:24:29.220Z
G. Sliepen
# How expressive of a type system is too expressive, for the average programmer?
Posted by: username_0 on 2023-08-23
The advantages of an expressive type system cannot be denied. The usual definition applies - how much valid behaviour a chosen system allows, while also preventing invalid behaviour.

In terms of "expressiveness" of type systems, i've come up with the follow (partial) hierarchy, where the intent is that each system allows more valid behaviour than the one before it. This is mostly based off the lambda cube. I'm also only considering "strong" type systems, so nothing like C's. Please also further note that this is not the only ordering of type systems - As per the lambda cube, any possible ordering would need to be inherently partial. In this case, I have tried to select type systems I have seen practically used by (somewhat) popular languages.

I am also excluding things like traits in this list, as they can be (mostly) trivially added to any of these in at least a limited way.

* No polymorphism, base types only : eg, STLC
* Rank-1 : OCaml
* Rank-2 : GHC Haskell w. -XRank2Types, MLF
* System F : GHC Haskell w. -XRankNTypes
* System Fω : Terms that depend on types, types that depend on types. GHC Core - one of the IRs of GHC Haskell.
* MLTT[1] / CIC[2] : Full dependent types. Agda/Coq/Lean/Idris.
* CTT[3] : Full dependent types, and higher inductive types. Cubical Agda is the only impl I am aware of.
* Something even more expressive i'm not aware of?

[1]: Martin-Löf Type Theory
[2]: Calculus of Inductive Constructions
[3]: Cubical type theory

My question is at what point has it been shown that the average user starts getting confused more often than not? While a stronger type system allows more valid behaviour, it also inevitably becomes more confusing - especially once you start to get into dependent type territory with Fω, so I wouldn't be surprised if this is that cutoff point.

Please note that I am not asking for personal opinions on the matter; if possible, any sort of quantitative evidence would be appreciated. I have tried various search engines to see if there is there is anything preexisting on the matter, but I have not found much, so I'm curious if anyone here has anything.
**Tags:** type-systems type-theory polymorphism dependent-types
> **Comments:**
> **username_1**: Judging from your hierarchy, it seems like a better term would be "expressivity" rather than "strength". I also don't see what this hierarchy has to do with "loopholes" ─ a language could have a type system in any of these categories, while also having (or not having) an escape hatch. It's also somewhat debatable whether your hierarchy really reflects type systems "prevent[ing] as many errors as possible"; for example any mistake possible to make in the simply-typed lambda calculus is also possible to make in a more expressive type system, if you just don't use the additional features.  
> **username_2**: The first paragraph seems to take "strong" in the conventional "strong typing" binary property sense, but the rest uses "strength" differently to mean comparable *degree* of complexity, expressivity, depth, or something else. I think it'd be clearer to tidy this up somehow with distinct terminology (although I'm not convinced that this *is* a total order either). For what it's worth, I don't believe that any such studies *have* been run, but in theory they could, so seeking that information is a fine question and I'd be interested in an answer to it.  
> **username_0**: @kaya3 Would a better wording perhaps be "Allowing as much as possible expressivity as possible within it's domain?" If so, please feel free to edit the question yourself, or I'll edit it when I have time.  
> **username_0**: @MichaelHomer In retrospect I agree. I'll edit the question as soon as I have some time to reword everything to not use "strong".  
> **username_3**: GHC Core, an important intermediate language used by the GHC Haskell compiler, essentially uses System Fω, AFAIK. Haskell itself, if you count extensions, *almost* has System Fω in the type system with its type families, but you there is no general-purpose type abstraction (`Λ`) and you can't straightforwardly fake it using type families.  
> **username_3**: I agree with @MichaelHomer that there probably isn't a total order for expressiveness. See, for example, [the lambda cube](https://en.wikipedia.org/wiki/Lambda_cube). That is an ordering on expressiveness that is not a total order. For instance, λP and λ2 are incomparable in the lambda cube ordering  
> **username_0**: @DavidYoung That's why i've presented at least one possible partial ordering here - I've tried to select the type systems that i've seen either practically used, or "inbetween" ones that are practically used. I've never seen a widely used language that uses either of λP or λ2, so I didn't include them. See your other comment for why I included Fω.  
> **username_0**: @DavidYoung I'll add GHC Core as an example for Fω, thank you.  
> **username_4**: Is the characterisation of OCaml correct? OCaml has objects and first-class modules, GADTs - not present for example in Standard ML.  
> **username_5**: The "average programmer" does not use OCaml or Haskell, let alone Agda/Coq/Lean/Idris. The average programmer uses Python, JavaScript / TypeScript, Java, Kotlin, C++, C, etc. So the language examples you state are in contradiction with the question. The fact that most mainstream languages have type holes does not make them uninteresting for the question. Furthermore, as far as my limited understanding of type systems goes, there are things you can type in these mainstream languages, that you cannot in Haskell: this is not a one-dimensional hierarchy.  
> **username_0**: @ChristianLindig While OCaml technically does have first class polymorphism (ie rank N) via the use of modules and records, I felt it more useful to only include the "standard" things an OCaml programmer would use, which is rank-1. (Also, GADTs and first class modules fall under the "traits" category above, ie they can be added to any of the systems). Don't worry, I'm not trying to mischaracterise OCaml; it's my day-to-day language ;)  
> **username_6**: You are missing out some orthogonal dimensions in typing, in particular the quantitative dimension (e.g. linear vs affine) and the parallelism dimension (e.g. session types).  
> **username_6**: There is a complementary dimension to your *what* type features are problematic, namely *when* do they start becoming problematic. To paraphrase a colleague: _types are like cocaine: you see the benefits immediately and you want more, but the problems only later_ ...  
> **username_7**: Judging from Go, many programmers consider enums and sum types too complex…  
---
## 2 answers
### Answer by username_8 on 2023-08-24. Score: 40 | Accepted answer
This is an interesting question, but I want to first break down the two big assumptions.

First, assuming the "average" programmer has some sort of type expressiveness limit is probably nonsensical. Otherwise, the answer seems to be that *every* type system is too expressive. The [2022 Stack Overflow Developer Survey](https://survey.stackoverflow.co/2022/#most-popular-technologies-language) indicates that over half of the top 10 languages have no static typing at all. The other half do not have very expressive type systems relative to your examples (except Typescript), and zero of them are sound. Additionally, the only research I could find into this mostly has to do with dynamic vs. static type systems (see [this thread](https://softwareengineering.stackexchange.com/questions/10032/dynamically-vs-statically-typed-languages-studies)), which signals to me that there isn't much literature on the subject yet.

Another problem here is that "moving up" to higher order type systems, while technically more expressive, has quickly diminishing returns regarding practicality in a real program. Pierce's [Types and Programming Languages](https://www.cis.upenn.edu/%7Ebcpierce/tapl/) briefly discusses this, saying

> A natural question at this point is “Why stop at three levels of expressions?” Couldn’t we go on to introduce functions from kinds to kinds, application at the level of kinds, etc., add a fourth level to classify kind expressions
> according to their functionality, and continue on in this way ad infinitum?
> Such systems have been investigated by the pure type systems community [...]. For programming languages, however, three levels have proved sufficient.

We can see this in modern programming languages. Haskell, for example, lowers to GHC Core, which is an augmented version of System F (it does not quite make it to F$\_\omega$). Simon Peyton Jones has a great paper on it, which you can read [here](https://gitlab.haskell.org/ghc/ghc/-/blob/master/docs/core-spec/core-spec.pdf). OCaml, and other ML languages, use a restricted version of System F. The only languages that offer more expressive type systems are almost entirely restricted to the domain of proof assistants.

So, if we are looking at current languages, it seems that F$\_\omega$ is pretty much the limit -- you don't hear a lot of people complaining that Haskell isn't expressive enough.

If you wanted to add more *real world* expressiveness to a type system, I would go about it by adding features, instead of adding another level of expression. Algebraic data types, type families, type classes, and GADTs, to name a few examples, can all be added to a system less powerful than F$\_\omega$. I would argue that these features increase real world expressiveness more than (for example) a 4 or 5 layer system ever would, and allow programmers to eliminate more classes of error, which I think is the real goal here.
> **Comments:**
> **username_0** (2023-08-24): For what it's worth, if the limit is "the average dev doesn't want to even handle a static type system, let alone a complex one", then i'm willing to accept that. Please also be assured that by "limit" I don't mean a conceptual one; i'm sure almost all devs would be able to *understand* the more complex half of this hierarchy if given time to learn it, but it's more about whether they're *willing* to, in which case an answer of "any static system" is a perfectly valid answer.  
> **username_4** (2023-08-24): The last paragraph is key. Having good base types, sums, products, ad-hoc and parametric polymorphism supported by syntax is more relevant than a theoretically more powerful system where everything is a lambda term (which is enough to study the expressiveness but not to build something).  
> **username_1** (2023-08-24): Welcome, and a great first answer! Totally agree about the last paragraph; for Typescript in particular, mapped and conditional types are excellent for expressing relations between types, so that if you want to change the design later you only have to change it in one place. And whlie it's technically outside of the type system, control-flow type narrowing is a feature which can make the type system more useful.  
> **username_9** (2023-08-24): @blueberry I think anyone operating in a non-pure research environment would have to ask the question "what benefits can *only* be achieved by this type system, and what commercial value do they have compared to the retooling cost".  
> **username_0** (2023-08-25): @pcj50 I would have hoped that was implicit in my wording above, but if it wasn't, I apologise for me not being clear.  
> **username_0** (2023-08-25): I'm going to accept this, as the community seems to like it and it contains some good information.  
> **username_10** (2023-08-28): "the average dev doesn't want to even handle a static type system, let alone a complex one" however, many devs prefer the benefits of static typing, and type inference is quite popular in newer languages, which gives the syntax of a dynamic language but the power of static typing  
> **username_0** (2023-09-01): @Seggan To say that type inference is popular in newer languages is a bit odd; ML has been around since '83 with full program type inference, and variants of said are still quite popular today. I'd say it's more accurate that people are only realizing how nice it is recently, not that it wasn't possible.  
> **username_10** (2023-09-01): I never said it wasn't *possible*. I said that just now it's beginning to drop up in the mainstream.  
---
### Answer by username_11 on 2023-08-24. Score: 17
Luke LaBonte already gave an excellent answer. I just want to add some things:

My question is at what point has it been shown that the average user starts getting confused more often than not?

I think people are generally confused in these two cases:

If the type system is introduced before you need it, and especially when it's not described using simple examples in your programming language. If I read articles about type systems that come from a functional programming perspective and that use some weird notation, my eyes glaze over.
When something that looks natural in your programming language to write, but then the compiler/interpreter does something unexpected or throws an error.

As an example of 1, introducing people to C++'s template system before they need it is a bad idea; they will probably dislike it and avoid it. However, if you tell them to write an implementation of a linked list of ints, and then ask them to make it work for float, std::string and ten other types, they will figure out that it would be really nice if that int could be replaced with some type variable, and then suddenly introducing the template notation seems logical. And suddenly they understand generic types.
As for 2, consider someone know that you can create arrays of a given length like std::array in C++. But now they have to read some data with variable length. It's then very natural to write:
std::size_t length;
std::cin >> length;
std::array my_array;

However, that will not compile, because C++ only allows types to depend on compile time constants, not on runtime values. The programmer will think: "why can't the compiler just do what I want?" With "what I want" being the possibility of having dependent types.

While a stronger type system allows more valid behaviour, it also inevitably becomes more confusing - especially once you start to get into dependent type territory with Fω, so I wouldn't be surprised if this is that cutoff point.

I agree with Luke that there is no such cutoff point. Rather, I think a programmer will at some point come upon a situation where they would need something that is obvious at the moment, but would be considered an advanced type system feature. The programmer also doesn't need to understand type theory as you would teach it at a computer science course, they just need to understand it in terms of how to use their programming language to achieve it.
---
