Spiffy GADT Thing

Take a look at this C++ code:

class Base {
  public:
    virtual ~Base() { }
};
class Derived : public Base {
  public:
    virtual void talk() { cout << "What's up?"; }
};
void test(Base* b) {
    if (dynamic_cast<Derived*>(b)) {
        b->talk();
    }
};

What’s wrong with it? Well, nothing really, it’s perfectly well-defined. Except it doesn’t compile. But at the time we get to the call b->talk() we know that b is actually of type Derived*, so we should be able to call talk() on it.

Now, I don’t expect languages to do this kind of magic. It’s perfectly reasonable for C++ to reject this code. But I was browsing the GHC source this morning and found a little hidden feature in the do notation. Haskell does do this!

Say we have this GADT:

data W :: * -> * where
    IntVal :: Int -> W Int
    AnyVal :: a -> W a

instance Show (W Int) where
    show _ = "W Int"

Then this code fails to compile:

test :: W a -> IO Int
test w = do
    print w
    IntVal i <- return w
    return i

Which makes sense, since w has type W a, and only W Int is an instance of Show. However:

test' :: W a -> IO Int
test' w = do
    IntVal i <- return w
    print w
    return i

Compiles just fine. That’s because if we got as far as the print w, then the pattern match succeeded, and thus w must be of type W Int as specified by the GADT. So imperative code in Haskell does narrowing, which most imperative languages don’t even do. Sweeet.

About these ads

3 thoughts on “Spiffy GADT Thing

  1. Given that you have to guarantee the correctness of the narrowing in the pattern before “print w”, how is this truly superior to changing the if-condition in the C++ code to (Derived* d = dynamic_cast<derived *>(b)) before invoking d->talk()?

  2. Tom, I’m not sure it’s superior, it’s just cool! I mean, if it were a huge win, more imperative languages would have done it, because it’s not that difficult to do in the limited way that Haskell does it. I’m presently infatuated with Agda (a completely unpractical, but very neato language), where you could abstract the cast and still get the assumptions: i.e. if isIntExpr w then print w else return () would work also. And that I can see as a win (not in this particular instance, just in terms of raw expressive power).

  3. To correct a minor typo, you need “IntVal” instead of “IntExpr” in the definitions of test and test’

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