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.
