# Subtypes as subsets of SML datatypes

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 lazy

structure 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 _ = NONE
end


As 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 ys


But 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 stream

subtype '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 stream
val exec : 'a executable -> 'a queue


However, 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?

These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements.

I can use GADTs, TypeFamilies, DataKinds, and TypeOperators (just for aesthetics) and create what you're after:

data Term0 varb lamb letb where
Lam :: lamb -> Term0 varb lamb letb -> Term0 varb lamb letb
Let :: letb -> Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb
Var :: varb -> Term0 varb lamb letb
App :: Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb

type Term b = Term0 b b b

data Terms = Lets | Lams | Vars

type family  t /// (ty :: Terms) where
Term0 a b c /// Vars = Term0 Void b c
Term0 a b c /// Lams = Term0 a Void c
Term0 a b c /// Lets = Term0 a b Void

Now, I can write functions with more refined types:

unlet :: Term b -> Term b /// Lets

• Thanks for your answer. I dislike GHC's TypeFamilies purely on principled grounds: it destroys parametricity and free theorems. I'm also not too comfortable with GADTs, because given a GADT Foo a, you can have two isomorphic types Bar and Qux, such that Foo Bar and Foo Qux aren't isomorphic. That contradicts the mathematical intuition that functions map equals to equals - and, at the type level, isomorphism is the right notion of equality. – pyon Jul 26 '16 at 15:41
• I understand your qualms, but it allows for specialized generalizations, something that I find quite valuable in practice. – Samuel Schlesinger Jul 27 '16 at 21:08