Getting clever with pattern matching

If I haven’t blogged much lately, it’s because I haven’t worked on Effes much lately. Some of it is because I’ve been busy, and some of it is because my current task is, well, a bit difficult. It’s been hard to find the time and energy to focus on it for more than a half-hour here or there, which is really what I need to do.

The problem I’m working on is pattern matching:

truthy : True | False
myValue = case truthy of
    True: 1
    _: 0

Okay, so that example is pretty easy. The problem is that I really want to disallow what Haskell calls partial functions: functions that might not apply to all inputs that the type system allows. Consider:

possiblyTruthy : True | False | Unknown
myValue = case possiblyTruthy of
    True: 1
    False: 0
    -- no match for "Unknown"

Haskell will happily compile the equivalent of this code, and unhappily throw a runtime exception if myValue is Unknown. For a language that prides itself on its awesome type system, that’s not super helpful!

The easy option is to require an “else” (_: foo) on all case expressions, but that’s annoying (or even dangerous) when you know (or think) that you’ve already specified all the possibilities. I want to do better: I want the compiler to know whether you’ve specified the possibilities. Specifically, I’d like it to require:

• that all possibilities are specified
• that nothing impossible is specified

To do this, I need a way of “subtracting” types.

t : True | False
myValue = case t of
    True: 1  -- t is now (True | False) - True,
             -- so t : False
    False: 0 -- t is now (False) - False
             -- so t : ()
    -- no need to specify a catch-all _: case

For simple expressions like this, the subtraction is easy. But it gets tricker when you allow more complex patterns, ones that let you peer into a value’s components. Consider:

Boolean = True | False
List[T] = Cons(head: T, tail: List[T]) | Empty
bools : List[Boolean]
v = case bools of:
    Cons(True, _): 0
    Cons(False, Cons(_, Cons(False, _))): 1
    Cons(False, Cons(_, Cons(False, _))): 2
    Cons(True, Empty): 3 -- error!
    _: 4

After the first pattern, bools is:

List[Boolean] - Cons(True, _)
=   List[True | False]
  - Cons(True, _)
=   Cons(True | False, List[Boolean]) | Empty
  - Cons(True,  _)

Let’s “factor out” the True | False from the first Cons. I’ll also use one-letter type names as shorthand, since this gets tricky: B for Boolean, T for True, etc.

=   C(T | F, L[B]) | E
  - C(T, _)
=   C(T, L[B]) | C(F, L[B]) | E -- factor out the T | F
  - C(T, _)
=                C(F, L[B]) | E

Okay, that wasn’t so hard. But then, the pattern I matched was pretty simple (“any list that starts with True). As the patterns get more complex, so does the logic; I might need to recurse down an arbitrary number of times on an given argument. I also need to do this lazily: List[T] is potentially infinite, so I can’t just factor everything out and subtract out the simple terms.

One way is to do a lazy breadth-first expansion: produce a sequence of types, each with one more layer expanded, and just keep going down that list until I either find the exact type I need, or find that it can’t possibly exist. That would work, but my spidey sense doesn’t like it. It feels like I should be able to hone in better on the expansions I actually want. That will probably also give me better error messages, if a user misses a possibility or types out something impossible (like the Cons(True, Empty) above, which is impossible since we’ve already covered all lists that start with True). I don’t think it’s super difficult; but it’s not trivial.