Haskell isn't "pure" static typing, but what should we call it then?

Learn
1

I know the static vs dynamic types debate has been won by the static typing folks; Typescript is increasingly common vs Javascript, and Python is now gradually typed with typecheckers.

However, I think it’s important to point out that, if gradual typing is dynamic typing moving toward static typing, then features like type inference, polymorphism, and so on, are static typing trying to move toward dynamic typing in terms of code reuse and general ergonomics.

The particular Haskell flavor of polymorphism, which has been described by Alexis King as “aggressively polymorphic”, needs some kind of description and needs to be recognized as a particular feature of Haskell, since it offers both advantages in improving code reuse as well as in ergonomics.

What should this be called? Or is “aggressively polymorphic static typing” good enough as a term?

1 Like
2
  • “and so on” includes what? In particular, the distinguishing feature of Haskell is typeclasses/overloading yet you don’t specifically mention that?
  • static typing entails type inference to errm statically errm infer types of all (sub)expressions without explicit signatures. (And to verify the correctness of explicit signatures.)
  • I don’t think of static typing as a "move toward"s anything. I don’t think dynamic typing is somehow ‘better’ or an end point for typing in general.
  • Static typing helps with code reuse and ergonomics because you can read the code errm statically, without having to imagine it executing.
  • But then many features of language design contribute towards those objectives, why call out (dynamic) typing specifically?
3 Likes
3

Static typing as a generic concept includes C, C++ (including auto), and Java. C at least is weakly typed with autocoercion, among other things, while Go used to lack generics.

The static vs dynamic typing debate comes down to performance + safety vs ergonomics.

What I am looking for in particular is to point out how Haskell’s particular brand of static typing is distinct from other forms of static typing (although it bears similarity to Rust’s traits, which, of course, lack HKTs but simulate it via GADTs), and how Haskell’s particular formulation allows Haskell, as a statically-typed language, to have some of the benefits of dynamically-typed languages in the same way as gradual typing allows dynamically-typed languages to have some of the benefits of statically-typed languages.

4

Isn’t Haskell already gradually typed language with -fdefer-type-errors?

Then I would promote Haskell as gradually typed, but with better defaults :slight_smile:

I actually use Haskell in this gradual typed way, at the beginning writing everything as Strings and Ints, passing stuff around as tuples, etc. Only to later introduce some newtypes, ADT and “aggressive polymorphism”.

“Fearless refactoring” makes Haskell “fearlessly gradual”.

1 Like
5

I’m actually curious about this, because I hear a lot about and can get some blogging details on the architecture war between “Simple Haskell / Handle Pattern”, “MTL / Classy Monads”, “Free Monads”, and “Algebraic Effect Systems”.

The “I wish Haskell were gradually-typed” / “Prototyping Haskell wants more flexible types” vs the “Standard Type-safe Haskell”, often with Type-Driven Development, vs the “Dependently Typed Haskell” war has much less coverage, with most people seemingly taking a position between “Standard Type-safe Haskell” vs “Dependently Type Haskell”.

But this is off-topic, I’m more looking to define “highly-polymorphic static typing” vs “Go has no generics”, “Dynamic Typing Supremacy”, and “Okay, so maybe a type checker on top of a dynamic language is a good idea”.

6

I think phrasing dynamic typing, gradual typing, and static typing as on a one-dimensional spectrum (the wording “move towards”) is a subtle form of false dichotomy (or alternatively a generalization of false dichotomy).

But you can try: polymorphic static typing.

1 Like
7

When comparing practical type systems in this day and age, I think a very important distinction is whether the types are enforced. In particular, if I have a function that declares its argument to be of type (non-null) integer, do I ever have to check whether I actually got an integer (or could a null/None etc. or a string ever slip through at runtime)? With today’s mainstream scripting languages that got slapped a type checker in front, you never have that guarantee. But in Haskell there’s no meaningful way you could get anything other than an Int if your argument is declared as Int. (I tend to keep bottom outside this discussion, but some may treat it as a null and I would definitely keep memory corruption outside this discussion)

I think this certainty of types have a very strong influence on how people use types. For example, in a Python codebase (even one that has fully embraced types), relying on type information alone doesn’t cut it, you must have 100% code coverage to have confidence that you won’t get a runtime error from adding an integer to a string. That’s why I think every Haskell codebase has 100% test coverage even without a test suite :slight_smile:

I would say not, -fdefer-type-errors is very different from gradual typing. In a scripting language with a gradual type system, you can declare the type of something as Any and then you can pass it to the print() function, and if it happens to be something that can be printed at runtime, it gets printed. You can’t do that with -fdefer-type-errors in Haskell. As soon as the expression with the deferred type error gets evaluated, you get a runtime exception, regardless of whether the runtime values would happen to have worked if you interpreted the Haskell code.

On the flip side, -fdefer-type-errors doesn’t make Haskell’s type system any less sound, because you never enable it in production, and you can completely ignore it as long as it’s disabled.

Having said all this, I think an important distinction that Haskell has over the type systems of mainstream languages (be it gradually typed scripting languages, or rigidly typed imperative languages like Java etc.) is that in Haskell you actually bother to “prove” things with types.

What I mean is that in mainstream languages, types are there to make sure that an argument is an int and not a string. The more advanced language features like generics etc. all work towards propagating this information from one place to another, but at the end of the day, it’s all about “is this an int or a string?”. In Haskell, you obviously get the “int or string” bit sorted out as well, but thanks to functional purity, parametricity and the advanced type system features like HKTs, GADTs etc. along with the culture of semantics and lawful programming, Haskell also allows you to express non trivial theorems about the code in its types and people do make use of this in real world production code.

1 Like