Restricted Data Types

With some spare boredom I had this morning, I was skimming the section on functors in RWH. A little ways down they introduce the type:

data Eq a => Bar a = Bar a
instance Functor Bar where
    fmap f (Bar a) = Bar (f a)

And point out how the constraint does not allow a valid functor instance. But what if it did?

What I’m getting at is that nobody ever uses constraints on data definitions like that, because they’re basically useless (AFAIK, they just impose the constraint on each constructor and nothing more). Perhaps they could work in this way: the mention of the type Bar a implies the constraint Eq a. Thus:

fmap :: (a -> b) -> Bar a -> Bar b

The caller already provides the dictionaries Eq a and Eq b for you, because the types “Bar a” and “Bar b” come from his environment. I’m not sure what I mean by environment there.

The time you would be required to provide a dictionary would be if you used a Bar in the body of a function without mentioning it in the type signature.

If this makes sense (I’m not convinced it does in the least), it might be a nice way to solve the class restriction problem.

About these ads

3 thoughts on “Restricted Data Types

  1. Hmm, I’m not sure this works.

    Consider this:

    fcompose :: Functor f => (a -> b) -> (b -> c) -> f a -> f c
    fcompose a2b b2c f = fmap b2c (fmap a2b f)

    broken :: Bar Int -> Bar Int
    broken = fcompose (+) ($ 1)

    Nowhere in the environment do you see a Bar (Int -> Int), and it’s impossible to construct one as there’s no Eq instance at that type. But inside the internals of fcompose you do need to construct a Bar (Int -> Int)!

  2. With GADT syntax this wart was fixed, and restricted data constructors can indeed include a dictionary:

    data Bar a where
    Bar :: Eq a => a -> Bar a

    This still doesn’t allow you to write the Functor instance, since there is no Eq b.

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