Assumption by any other name make an ass of u and mptions

Until now, I've been using the term "assumption" to describe several ideas: interfaces that define behaviors, stateful traits that include implementations, polymorphism and more. Why haven't I used more standard terminology?

Before I get there, a slight diversion. People who work in Java will sometimes ask a question along the lines of, "I want a Map<K,V> where the keys can be of any type, and the values will depend on the key type." For instance, an Integer key would correspond to a value of MyVal<Integer> (for both gets and puts), a String key would correspond to MyVal<String> values, and so on.

The short answer is that you can't define a Map of that sort in Java. The next question is: why not? Isn't that reasonable? And then the real answer comes in: a type system is just a limited theorem checker, and we've known since Turing that we can't come up with an algorithm that will prove everything you want to prove; so we'll always have to draw a type system's line at some place, and this is where we happened to draw it. If Java allowed for those kinds of types, there'd always a slightly more sophisticated use case that you could ask about and wonder why not.

That got me thinking: what if I designed a type system that, though still limited, had an expanded scope? Most type systems define what types a given object can work with (based on its type). What if I designed one that defined what values an object can work with?

Take a quicksort as an example. The "main" recursive step will look something like:

return (quicksort left) + pivot + (quicksort right)

Well, what happens if you get confused (it's late and you're watching TV while coding) and instead flip the two sides:

return (quicksort right) + pivot + (quicksort left)

My idea was that you could define an assumption called Sortable that would describe which values can be, for instance, pushed into a stack:

Sorted Stack[A] requires A :: Ordered st
    push a requires
        size == 0 or
        a >= pop

Now, in order to push into a Sorted Stack[A], firstly the A type has to have an ordering defined (as it does in any statically typed language that would deal with sorted structures), and secondly, you must have proven in the code that the input is >= the stack's head. For instance:

A :: Ordered ->
badPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    push s v -- compilation error!

A :: Ordered ->
tryPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    if (size s == 0) or (v >= pop s)
        push s v
    else
        s

In the first example, the code couldn't prove that the assumption required of a Sorted Stack[A] is true, so the code failed to compile. In the second example, it could prove it, and everything's fine.

So, that's why I went with the term "assumption." The idea was that the basic components of a program wouldn't be types, but a bunch of assumptions of a more general nature asserted on objects.

The more I played with it, though, the less promising it looked. All but the most trivial examples became too difficult to express, and I kept needing an "escape hatch" for assumptions that would be cumbersome or impossible to prove in the code. The escape hatch would be in the form of telling the compiler, "I know you can't prove this, but trust me on it." Basically, I felt that the escape hatch would be needed so much that it would become the primary form of typing, in which case the language effectively becomes a dynamically typed language that requires static compilation — the worst of both worlds.

So, I've decided to abandon this effort, and instead focus on a more standard definition of types. I'm going to call these traits, though they're different from traits in some other statically compiled languages in that they're attached to individual objects, and not to other types (as they are in Scala, for instance).