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
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,
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:
= 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.