I think it's worth talking about the ability to propagate user-defined invariants. To me the most useful aspect of a type system is that it enables you to declare that all Xs have some property, and then the language guarantees that this holds. "Has a method named .foo(...)", while useful, shouldn't be the end of what we try to encode, but there's a big gap between allowing things like "an X is either a Y or a Z" and allowing arbitrary type-properties, liquidhaskell style, which the article just glosses over.
Which is a shame, because it's precisely this range - the gap between non-liquid Haskell or Ocaml and Java - which is most relevant to today's programmers making choices of programming language.
Yes, I've long wanted to be able to attach arbitrary predicates to types. This is great for functional state machines; say the state machine type is sm, you can specify functions like
fun initialize(sm) -> sm'
where sm.state == uninitialized, sm'.state != uninitialized
or
fun ping_clients(sm) -> sm' where has_clients(sm)
in concert with
fun has_clients(sm) -> bool
The compiler can then track these, and ensure e.g. that "has_clients" is called and returns "true" before "ping_clients" is called on a given value.
An even smarter compiler can, if it knows the definitions of these functions, determine statically whether a given predicate is guaranteed to produce the same result on a modified object. (e.g. simply by inspecting which fields are inspected and modified)
You can get this example working with indexed monads in Haskell. You can also do it quite nicely in dependently typed languages like Idris/Agda.
However, abitrary predicates is a different matter. Even if you have a language which allows arbitrary computation in types there exist undecidable predicates which may weaken your desire for arbitrary ones.
It seems to me that you probably don't want to do arbitrary computation in types at compile time. Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid. That's not a good position to put your compiler in.
It seems to me to be better to make this a runtime check, which the compiler makes sure to call every time subtraction is applied to a value of that type.
> Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction.
Well, no.
Its a problem if you assert that the result of subtraction is the same type, because the non-negative integers are not closed under subtraction--if the definition of your data type relies on something that is internally incoherent, you have a problem; but you can define subtraction of non-negative integers in a way that is general, not problematic, and doesn't require compile time knowledge of specific values, e.g.:
data Nat = Zero | Succ Nat
data Neg = Neg Nat
subtract :: Nat -> Nat -> Either Nat Neg
But, yeah, attaching arbitrary predicates as restrictions to types brings the halting problem into your compiler implementation.
> data Nat = Zero | Succ Nat
> data Neg = Neg Nat
> subtract :: Nat -> Nat -> Either Nat Neg
I think that this is one example where the types don't speak completely for themselves. Is `Neg Zero` meant to stand for the integer `0` (as one might naïvely expect) or the integer `-1` (as one might expect from the pseudocode `Neg n = -(n + 1)`)? If the former, then what is `subtract Zero Zero`? (I.e., is it `Zero` or `Neg Zero`? I hope that we don't get into IEEE 754 (http://en.wikipedia.org/wiki/Signed_zero) territory here!) If the latter, then there's no ambiguity, but I think that it's fair to say that that meaning isn't clear just from the type!
For minimum insanity, I think you'd have to assume that I meant Neg Zero to represent -1, Neg (Succ Zero) to be -2, etc., with an appropriate definition of subtract.
Well, you'd probably have to introduce a type such that every time you subtracted n from m you must prove that m is at least as big as n. Which would be a pain.
As usual, I really suggest playing with Agda or Idris to get a feel for what sophisticated types actually look and feel like.
which could either succeed or fail to produce the needed proof at runtime. Without the proof it'd be impossible to perform the subtraction, so that branch of your program is statically inaccessible.
I think even better is to have a subtraction that returns a different type, where you can't prove that a > b. Where you can, I don't know that I object to the compiler tracking such things, though I also don't actually use a dependently typed language.
"Even "this type is an integer that must be non-negative" is a problem if that type allows subtraction. Now your compiler needs to know the the value of all such types at the time that subtraction was applied to them, to know if the operation is valid."
This is one of the common misconceptions about the stronger-typed languages. I know because I had it before I learned Haskell. To say that you have a guaranteed non-negative number does not necessarily mean that if you subtract two such numbers that the compiler must be able to prove on the spot that the result is positive.
What exactly it means depends on the language. Haskell is not particularly capable of representing that type (or at least, simple Haskell is not), so it'll happily let you write:
and then simply propagate the incorrectness if you do end up with a negative number, doing whatever the underlying system does. But a programmer will notice this, and a correct subtract implementation may be:
in which case the compiler isn't doing anything, really; the implementation will examine the two numbers and return Nothing if the subtraction is invalid.
In Haskell, this is a runtime check... it is simply one you can not ignore. It isn't an exception (very easy to forget to check for), and you can't use the result (if there is one) until you unwrap it, and the language syntax to do so tends to strongly encourage you to handle the error. You can not subtract two such numbers without having it shoved in your face that it may fail. You may then choose to fail to check it, since the language can't actually stop you, but you will be doing so with full knowledge of the fact that you are doing so.
And in general, that's how a lot of the "bad computations" that a type system prevents is done... it isn't "prevented" so much as "you are forced to deal with violations". For instance, imagine you are deserializing input from an external source... in a strongly-typed language, all the deserialization routines will have Maybe (or perhaps Either with errors) pervasively used, since deserialization routines are able to fail at pretty much any point. The language doesn't prevent failures from happening, because it can't. It prevents you from sweeping failures under the rug, accidentally or otherwise.
Thus, in Haskell, the first subtract example up above, while the compiler won't actually stop you from writing it, is incorrect; there will exist no implementation that doesn't behave badly for some inputs. In a dependently typed language, there exist safe implementations, but you will have to provide some sort of proof that it works. However, since in general it's difficult to prove, that would probably involve some local context, and it's not hard to imagine that in practice for such a simple thing you might still end up using the equivalent of the Haskell function. It just depends on what you have in hand.
In a way, programming in something like Go has a very similar feel in this way to programming in Haskell, where the fact that the error is constantly shoved in your face and you are forced to deal with it before moving on is the way it generally works. Haskell has a wide variety of clever ways of dealing with it, and Go mostly uses brute programmer force, but the feel is quite similar, IMHO.
It's also worth noting semantically what the type of `subtract` reads as. It says that for any two NonNegative typed values you can produce a new value in the type `Maybe NonNegative` which is the type of NonNegatives adjoined with one special "failure" value.
So this is a perfectly well-defined notion of subtraction on non-negative numbers. It reflects the obvious fact that NonNegatives are not closed under subtraction.
Common Lisp supports arbitrary type predicates, and I think that SBCL enforces them (not sure) at runtime. For instance, it will call the predicate before setting a struct's field to make sure that it returns true (under high safety compilation, low safety just trusts that it's correct)
Which is a shame, because it's precisely this range - the gap between non-liquid Haskell or Ocaml and Java - which is most relevant to today's programmers making choices of programming language.