Related to my previous post on Skolem constants, another interesting issue related to type annotations is the direction the type information moves.
Now, there are at least two things I could mean by direction. On the one hand there’s what I will call the monadic typing direction, related to how we thread the substitution list through the abstract syntax tree. Generally this can be done left to right, depth first. (Is there any situation where we would choose otherwise? The principle reason to pick a different order, as far as I can tell, is that it may change where type errors show up in the code. ‘where’ clauses are about the only things I can think of that demand a different ordering, and they are usually desugared.)
Another possible meaning for direction is what I will call the polarity of type propagation. If you were to sit down and write a type inference algorithm, you’d probably write down some sort of type like
typeCheck :: Expr -> Env -> SubstitutionContext -> (Type, Errors, SubstitutionContext) or for the monadically inclined, typeCheck :: Expr -> Env -> SubstitutionContext (Type, Errors)
Since, we’re doing type inference, right? We don’t know what type an expression is, until we ask, so it should be a result, right?
Well, type annotations throw all that out again. Now we’d write something like this, instead:
typeCheck :: Expr -> Env -> Type -> SubstitutionContext Errors
Why? Well, given the type annotation, we need to pass that information down to the children, so they can use it. First, because that’s how we’re going to get those Skolem constants to work. Second, because many advanced typing features we’re going to want to add later might require this information to be given to the children. (For example, we need a type annotation to pass type information down to a pattern matching expression if we have GADTs or their equivalents in the language.)
But, how do we find out the type of a child? Well, you told it what type it was. Use that. (In a situation where you actually don’t know the type of a child, you gave it a variable. So, go apply the substitution context to that variable to refine it to the answer.)
Here’s a sample bit of pseudocode for how we might implement type checking/inference on a few types of expressions:
typeCheck (ifExpr cond then else) env type = do typeCheck bond env BooleanType typeCheck then env type typeCheck else env type typeCheck (appExpr func parm) type = do tv <- freshTypeVariable typeCheck func env (ArrowType tv type) typeCheck parm env tv typeCheck (absExpr var body) env type = do tv1 <- freshTypeVariable tv2 <- freshTypeVariable unify type (ArrowType tv1 tv2) typeCheck body (bind var tv1 env) tv2 typeCheck (trueExpr) env type = do unify type BooleanType
Note: If we were especially concerned about error messages, we might create a freshened version of ‘type’ for each then/else branch, then unify all three together in the end, ensuring they agree. (This way we’d get a special error for “then/else don’t have the same type” instead of pushing the error somewhere into the else branch, implicitly assuming the then branch is correct.) But I’m pretty much ignoring error messages in the above. It’s just another implementation detail that’s not so implementation detaily!
Note 2: Damn, my “high-level pseudo-code” is almost valid Haskell! I really need to get nicer support for monads into Silver, so the real implementation can look that good, but I guess it’ll be awhile before I get to it. :(
Anyway, here’s the punch line that got me writing this whole thing: you don’t need to find out the type of a child expression. All that happens instead is that the type errors get generated by the introduction forms of types, instead of their elimination forms.
Look at if and application. They don’t do a single bit of unification themselves. ‘if’ is how we eliminate the Boolean type, and application is how we eliminate the arrow type. Now look at abstraction and True. Both introduce a type, and both must have ‘unify’ calls as a result.
If we had written it the other way, where the Type is a result of the typeCheck call, it would be the other way around. There’s nothing that could ever be a type error about writing ‘True’, it’s just a boolean. But now, we have to have that check somewhere, so it ends up in the if expression: (I’ll just give the one example)
typeCheck (ifExpr cond then else) env = do condtype <- typeCheck cond env unify condtype BooleanType thentype <- typeCheck then env elsetype <- typeCheck else env unify thentype elsetype return thentype typeCheck (trueExp) env = do return BooleanType
I hadn’t noticed that the calls to unify showed up exclusively in one polarity, until I had to change the code to work the other way around and realized everything just flipped. Neat.