30
$\begingroup$

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.

$\endgroup$
14
  • 8
    $\begingroup$ 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. $\endgroup$
    – kaya3
    Aug 23, 2023 at 23:37
  • 1
    $\begingroup$ 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. $\endgroup$
    – Michael Homer
    Aug 23, 2023 at 23:46
  • 1
    $\begingroup$ @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. $\endgroup$
    – blueberry
    Aug 24, 2023 at 0:43
  • 16
    $\begingroup$ 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. $\endgroup$ Aug 24, 2023 at 10:39
  • 2
    $\begingroup$ @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 ;) $\endgroup$
    – blueberry
    Aug 24, 2023 at 22:56

2 Answers 2

38
$\begingroup$

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 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), 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 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. 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.

$\endgroup$
9
  • 3
    $\begingroup$ 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. $\endgroup$
    – blueberry
    Aug 24, 2023 at 4:28
  • 9
    $\begingroup$ 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). $\endgroup$ Aug 24, 2023 at 8:58
  • 3
    $\begingroup$ 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. $\endgroup$
    – kaya3
    Aug 24, 2023 at 12:26
  • $\begingroup$ @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". $\endgroup$
    – pjc50
    Aug 24, 2023 at 14:50
  • 2
    $\begingroup$ I'm going to accept this, as the community seems to like it and it contains some good information. $\endgroup$
    – blueberry
    Aug 25, 2023 at 1:43
15
$\begingroup$

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:

  1. 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.
  2. 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<typename T> 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<int, 10> 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<int, length> 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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .