Hacker News Reader

Comment by pydry | Hacker News Reader

I think there's a sharp rule of diminishing returns the stronger you make type systems. Type safety comes at a cost and that cost has to come with an associated payoff.

This is why ultra strong type systems end up being little more than academic toys - the payoff when you dial type safety up to an extreme doesn't match the associated cost.

Types and tests should meet somewhere in the middle because the same law of diminishing returns affects tests in reverse. They tend to be good at what the other is bad at and if you rely too heavily on one at the expense of the other they will start fraying around the edges.

View on HN

Indeed. A type means assigning a rigid category to something.

There is not a single taxonomy that is universal, it ends up like the Celestial Emporium of Benevolent Knowledge that decides animals into:

    those belonging to the Emperor,

    those that are embalmed,

    those that are tame,

    pigs,

    sirens,

    imaginary animals,

    wild dogs,

    those included in this classification,

    those that are crazy-acting,

    those that are uncountable,

    those painted with the finest brush made of camel hair,

    miscellaneous,

    those which have just broken a vase, and

    those which, from a distance, look like flies.

Then you have a new use case.

In Idris you get to choose how strict you want to make your types. E.g. you can choose to use "Vect n a" if you want a vector a's where the size is tracked by the type system. Or you can use e.g. "List a" if you want a list of a's where the size is not tracked by the type system.

Of course the problem comes when you have to interface some code which expects a "Vect n a" and you have a "List a", but that's solvable by simply checking the size (dynamically) and deciding what to do if your "List a" isn't of size exactly n. (Fail, or whatever.). Going from "Vect n a" to a "List a" is trivial, of course.

... but really, that's where most of the friction is: Boundaries between APIs where the types don't quite line up. (Which is often the case for other languages, tbf. We tend to just notice less at compile time since most languages are so bad at expressing constraints.)

What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?

"plenty" is relative.

You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.

I don't see many GAFAM products created in any functional language, even those with primitive type systems. Are you sure it is the type system that is scaring people away?

I was thinking of Haskell and F#. Neither one is completely unused outside of academic contexts but it is rare.

Rust is an example where a stronger type system has an associated payoff and it's being used all over.

Reply on news.ycombinator.com