Where Do Type Systems Come From?

Today less than 1% of all software is written in null safe languages. But I believe Swift has non-nullable types, and it's the promoted language for a really big ecosystem. There's also Rust and Scala, but those have less of a captive audience. I do have high hopes for Rust, which also is data-race safe.

I think Java 8 and optionals show it doesn't have to be that hard, it's just that there's too much old code that relies on nulls for the Java ecosystem to ever be fully null safe.

Use-after-free is solved in a language without manual memory management, so that's actually quite common.

Programmers get comfortable with new ideas over time. Higher order functions and type inference used to be obscure concepts. Today they're par for the course. I don't know if we'll all use dependent types some day, but I think we'll keep getting more powerful types in mainstream languages for a while.

    foo :: a -> (b -> c)

Not saying it's wrong, but "foo is a second-order function" is a distinctly minority opinion.

To a useful first approximation, Haskell works as a cartesian-closed category, which basically means we have tuples and that tuples harmonize with functions so that foo behaves just like

    uncurry foo :: (a,b) -> c

which is a first-order function.

So the majority opinion calls foo a first-order arity-2 function.

Here's a bar function that's truly second-order:

    bar :: (a -> b) -> c

In general, the order of a function is the count of parens nesting the leftmost innermost arrow. It is invariant to currying/uncurrying as well as permutation of arguments.

The same counting principle applies to other invariants such as ranks and kinds.

"How high can the order of a function go?" is the question explored in this blog post [0]. Note how the author's definition of order -- essentially the same given here -- got left and right mixed up.

[0] http://math.andrej.com/2006/03/21/interesting-higher-order-f...

Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue.

For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case.

Or consider a program like:

    x = 1
    print_int(x)
    x="a"
    print_string(x)

I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify.

Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it).

You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior.

A completely different type of example, is C code such as:

    *0x01 = 0

which means "set the memory at address 1 to 0", but is poorly typed.

What a great piece!

I wish the author would expand on this piece with either more installments or a even short book.

I find myself interested in type systems as it relates to programming language design but I haven't found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this article.

Can anyone recommend any other such middle ground resources on type systems and type system theory?

>"Distinctly unimpressed by this post. The author seems to have an axe to grind with mathematicians as a class, which, as we would have been told in school, isn't 'big or clever'."

I thought it was intended to speak to people who might be intimidated or feel obtuse when they encounter really dense academic texts when trying to learn more about type systems as it relates to programming. As such I really appreciated it.

I didn't think the author was grinding any axes at all, quite the contrary.