Type guards are not inferable

Type guards, or typecase expressions allow refining a binding’s type and are commonly used in dynamic languages such as JavaScript. Consider (adapted from Simple Unification-based Type Inference for GADTs):

f x y = typecase x of
            Int -> i + y
            other -> 0

The function can have either of these two types (among others):

a -> Int -> Int


a -> a -> Int

Neither is more general, so there is no principal type.

Unless the user tells us something (in a type annotation) we have no way of deciding which type should be inferred.

So for now, Infernu will probably not have support for type guards like Flow and TypeScript do (both of which don’t have full type inference). Another possibility is to allow type guards in trivial cases only.

Type guards are not inferable

2 thoughts on “Type guards are not inferable

  1. anbaric says:

    Have you looked at OCaml’s approach (“Tracing ambiguity in GADT type inference”, Jacques Garrigue & Didier Rémy)? It seems to solve a similar problem (though not in an entirely satisfying way).

    1. Thanks! I wasn’t aware of that paper.
      I’m trying for zero annotations at this point, but maybe following that paper’s idea there’s a way to detect unambiguous cases and infer at least those.

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 )

Google+ photo

You are commenting using your Google+ 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 )


Connecting to %s