Type checking polarity

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.

Advertisements
This entry was posted in Compilers, Typing Tidbits and tagged . Bookmark the permalink.

One Response to Type checking polarity

  1. You should check out bidirectional type inference, which alternates between inference and checking (which relates to whether the types are being pushed down or pulled up). There’s a lot of research on different bidirectional approaches.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s