Demand Driven Refinement Types?

I was a little bored last night, and while drifting through thoughts, figured I should take a look at what all this refinement type stuff was about so I'd have a better feeling for when to give it a real look.

The first example in Tim Freeman's thesis "Refinement Types in ML" demonstrates a (recursive) function to pull out the last element in a linked list (well, cons cell, I'm doing element). Using ML pattern matching sugar, we can cleanly describe the recursive and base cases, and ignore the case of an empty list (with no last element) as it is undefined in the function:

datatype 'a list = nil | cons 'a * 'a list
fun lastelt
cons(val, nil) = val
| cons(_, rest) = lastelt rest

The type of lastelt isn't " 'a list -> 'a ", because lastelt isn't defined for nil lists. We could say it is defined on non-nil lists, which is fair. How about if we returned the second to last element in our function? Given our datatype, we want to cut it up a little differently, and define refinement types. The thesis then shows a refinement type to augment the above code:

rectype 'a empty = nil
and 'a singleton = cons('a, nil)
and 'a long = cons('a, cons('a, nil))
(* ... however many other refinements ... *)
and 'a all = bottom (list) **

Now, we can say which refinements our function is defined on. In spirit, at least, refinement types provide a way to guide abstract interpretation style type inference: we track how operations (constructing cons cells and destroying them) interact in terms of our rectypes. It provides a separate, but similar, axis of hints for our inference algorithms.

While I was originally keeping this work filed away as being a potential tool to look into if I were to work on mutation/references or expressive type systems, it seems relevant to much more, and pose a few questions.

For starters, in the case of refinement types for recursive data structures, are explicit refinement types really necessary for an inference algorithm? Evan has been rocking recently with shape analysis via inductive proofs using separation logic (coming to a POPL near you); an analogue might be possible here. If inference fails to unify due to a missing case, expand to catch it. The trick then would seem to be on how to detect fixed points when expanding the refinement types. This probably stinks algorithmically, but it's a start :)

Anyways, refinement types seem neat, and this has been a pleasant reminder in why examples help, choosing a good example is important, and why, given time, I prefer to read a thesis over a conference paper. As for the example bit, a good example should help demonstrate not just the solution, but also the problem. I'm struggling a little with that in my paper right now - paper length requirements force you to think :)

**Even without having read significantly further, I suspect this last line is unnecessary wrt the lhs, and the rhs seems odd though sound in the lack of parameterization, but either way, it isn't too relevant.