One of the few things that I dislike about Okasaki's book on purely functional data structures is that his code is littered with inexhaustive pattern matching. As an example, I'll give his implementation of real-time queues (refactored to eliminate unnecessary suspensions):infixr 5 :::datatype 'a stream = Nil | ::: of 'a * 'a stream lazystructure RealTimeQueue :> QUEUE =struct  (* front stream, rear list, schedule stream *)  type 'a queue = 'a stream * 'a list * 'a stream  (* the front stream is one element shorter than the rear list *)  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)    | rotate (Nil, y :: nil, zs) = y ::: $zs  fun exec (xs, ys, _ ::: $zs) = (xs, ys, zs)    | exec args = let val xs = rotate args in (xs, nil, xs) end  (* public operations *)  val empty = (Nil, nil, Nil)  fun snoc ((xs, ys, zs), y) = exec (xs, y :: ys, zs)  fun uncons (x ::: $xs, ys, zs) = SOME (x, exec (xs, ys, zs))    | uncons _ = NONEendAs can be seen rotate isn't exhaustive, because it doesn't cover the case where the rear list is empty. Most Standard ML implementations will generate a warning about it. We know that the rear list can't possibly be empty, because rotate's precondition is that the rear list one element longer than the front stream. But the type checker doesn't know - and it can't possibly know, because this fact is inexpressible in ML's type system.Right now, my solution to suppress this warning is the following inelegant hack:  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)    | rotate (_, ys, zs) = foldl (fn (x, xs) => x ::: $xs) zs ysBut what I really want is a type system that can understand that not every triplet is a valid argument to rotate. I'd like the type system to let me define types like:type 'a triplet = 'a stream * 'a list * 'a streamsubtype 'a queue of 'a triplet  = (Nil, nil, Nil)  | (xs, ys, zs) : 'a queue => (_ ::: $xs, _ :: ys, zs)  | (xs, ys, zs) : 'a queue => (_ ::: $xs, ys, _ ::: $zs)And then infer:subtype 'a rotatable of 'a triplet  = (xs, ys, _) : 'a rotatable => (_ ::: $xs, _ :: ys, _)  | (Nil, y :: nil, _)subtype 'a executable of 'a triplet  = (xs, ys, zs) : 'a queue => (xs, ys, _ ::: $zs)  | (xs, ys, Nil) : 'a rotatable => (xs, ys, Nil)val rotate : 'a rotatable -> 'a streamval exec : 'a executable -> 'a queueHowever, I don't want full-blown dependent types, or even GADTs, or any of the other crazy things certain programmers use. I just want to define subtypes by carving out inductively defined subsets of existing ML types. Is this feasible?
Subtypes as subsets of SML datatypes
type theory;type inference
These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements. They were introduced by Tim Freeman and Frank Pfenning, in their 1991 PLDI paper, Refinement Types for ML. Rowan Davies studied type inference for refinement types in his PhD thesis, Practical Refinement Type Checking. He also implemented it as an extension to SML, but I don't know if it is available online.Joshua Dunfield studied how to combine datasort refinements with fancier lightweight type dependency in his thesis, A Unified System of Type Refinements. He also implemented it in his Stardust language, which is available online:http://www.mpi-sws.org/~joshua/stardust/