typeclasses and type constraints

[Phaedon Sinis]

Hi all,

I've been stuck on this issue for several hours while trying to refactor my project prototype to use all sorts of nice abstractions.

I'm experimenting with creating a tree representation of an image:

data ImageTree2d c

     = Leaf { imageFn :: Point2d -> c }

     | Unary { unaryOp :: (Color ci) => ci -> c, -- yeah, it's different b/c maybe we're going to another color space

               treePtr :: (Color ci) => ImageTree2d ci  -- but gosh I wish I could bind this to the same "ci" as in unaryOp

               }

     | Binary { binaryOp :: (Color ci) => ci -> ci -> c, -- same here

                leftPtr :: (Color ci) => ImageTree2d ci,

                rightPtr :: (Color ci) => ImageTree2d ci 

                }

     | Spatial { xformFn :: Point2d -> Point2d ,

                 streePtr :: ImageTree2d c}

so we can build up a "image processing tree" of compositing ops, color processing ops, and spatial transformations. The original image is a simple function and sits in a leaf. 

Cool, so now I want to fmap -- for each pixel in my image, do some color transformation. Since we're not actually applying the transform, we just wrap it in a node with a pointer to the original tree:

-- | Defines pointwise operations on images!                                                                                                                                                                    

instance Functor ImageTree2d where

         fmap f imgTree = Unary f imgTree

And, fail!  I've tried removing and adding type constraints, but to no avail. I suspect there is a problem with the issue I point out in the comments above under "Unary". Am I thinking about fmap incorrectly, or is my tree idea fundamentally flawed? I thought that parameterizing by color could be awesome, but I'm open to suggestions. 

src/Hip/Image.hs:81:33:                                                                                                                                                                                         

    Could not deduce (a ~ ci)

    from the context (Color ci)

      bound by a type expected by the context: Color ci => ci -> b

      at src/Hip/Image.hs:81:27-41

      `a' is a rigid type variable bound by

          the type signature for

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

          at src/Hip/Image.hs:81:10

      `ci' is a rigid type variable bound by

           a type expected by the context: Color ci => ci -> b

           at src/Hip/Image.hs:81:27

    Expected type: ci -> b

      Actual type: a -> b

    In the first argument of `Unary', namely `f'

    In the expression: Unary f imgTree

[Drew Haven]

So, after looking at your code.  At first I'm struck that your ci variables don't seem linked. I think you want something more like:

data (Color c) => ImageTree2d c =

  Leaf { imageFn :: Point2d -> c }

  | forall ci. (Color ci) => Unary { unaryOp :: ci -> c

                                   , treePtr :: ImageTree2d ci

                                   }

  | forall ci. (Color ci) => Binary { binaryOp :: ci -> ci -> c

                                    , leftPtr :: ImageTree2d ci

                                    , rightPtr :: ImageTree2d ci

                                    }

Which requires Rank2Types and GADTs extensions I think.

Unfortunately I don't know how to bind "fmap = Unary" because fmap doesn't have any type restrictions but Unary does, and in fact you want to force the types to be constrained .  There has to be a way to set that up though.  I'll defer to the experts.

Drew Haven
drew....@gmail.com

[Ling Yang]

Unary is a data constructor taking a function of type (Color ci) => ci -> b.

Instancing Functor requires that fmap is over _arbitrary functions (a
-> b). Because this is more general than (Color ci) => ci -> b, you're
not allowed to do that; letting the instance pass the typechecker
would allow mapping functions f whose input (type ci) is _not_ of the
Color typeclass.

Think of (Color ci) => ci -> b as reading, mathematically, for all ci
in the set InstancesOfTypeClassColor, this type checks if it's a term
of type ci -> b.

Some quick workarounds:

1. Relax the type constraint on Unary.
2. Make your own typeclass Functor that uses a Color ci restriction.

On Fri, Nov 4, 2011 at 2:47 PM, Phaedon Sinis <phaedo...@gmail.com> wrote:

[Bryan O'Sullivan]

On Fri, Nov 4, 2011 at 2:47 PM, Phaedon Sinis <phaedo...@gmail.com> wrote:

data ImageTree2d c

     = Leaf { imageFn :: Point2d -> c }

     | Unary { unaryOp :: (Color ci) => ci -> c, -- yeah, it's different b/c maybe we're going to another color space

               treePtr :: (Color ci) => ImageTree2d ci  -- but gosh I wish I could bind this to the same "ci" as in unaryOp

               }

     | Binary { binaryOp :: (Color ci) => ci -> ci -> c, -- same here

                leftPtr :: (Color ci) => ImageTree2d ci,

                rightPtr :: (Color ci) => ImageTree2d ci 

                }

     | Spatial { xformFn :: Point2d -> Point2d ,

                 streePtr :: ImageTree2d c}

The root of your problem is that you're using typeclass constraints in your type definition above. By using those constraints, you "infect" all functions that operate on ImageTree2d with those constraints, regardless of whether or not said functions actually care about those constraints. This is why you can't write an fmap definition, because your constraints make it impossible to make the type of fmap polymorphic enough.

That problem is sufficiently pernicious that it's planned to remove the ability to add constraints to types from the language entirely at some point. In the mean time, remove the constraints above, add them to the functions that care about them, and leave it at that.

[dm-list-clas...@scs.stanford.edu]

At Fri, 4 Nov 2011 15:42:46 -0700,

Bryan O'Sullivan wrote:
>
> That problem is sufficiently pernicious that it's planned to remove the
> ability to add constraints to types from the language entirely at some point.
> In the mean time, remove the constraints above, add them to the functions that
> care about them, and leave it at that.

Just to add to Bryan's point, class constraints in data declarations
do not cause a dictionary to be placed in the data type. So they are
a) kind of useless, and b) contradict your intuition. All they do is
prevent code from compiling, but not ever actually allow anything new.
(Well, there are a couple of very fringe edge cases involving
defaulting or not of types like Num, but for the most part class
constraints in data declarations affect only the correctness, not the
semantics of code.)

Here's a prime example of why such constraints can be really
frustrating:

data (Show a) => Foo a = Foo a

instance Show (Foo a) where
show (Foo a) = "Foo " ++ show a -- compilation failure

This gives a compilation error saying "No instance for (Show a)".
Intuitively, a reasonable reaction might be, "What do you mean no
instance for Show a? Foo a *requires* a to be in class Show, so you
know a has to be in class Show? Why are you rejecting this code?"

The reason the code has to be rejected comes back to what I said in
lecture about always imagining that class constraints are hidden
dictionary arguments. Say you have a function like:

showFoo :: Foo a -> String
showFoo (Foo a) = show a -- error

This function has no (Show a) => constraint. Therefore, it does not
receive the Show dictionary for a. Therefore, it has no way of
calling the show method on a. Even though the compiler knows that
such a method exists, it doesn't have a pointer to it.

The solution, of course, is to say:

instance (Show a) => Show (Foo a) where
show (Foo a) = "Foo " ++ show a

But if you are going to sprinkle (Show a) constraints throughout all
your functions anyway, there's really not much value in having the
constraint also appear in the data type.

That said, if you want to pass a dictionary around explicitly, there
is a language extension called ExistentialQuantification that allows
you to do this. For example:

{-# LANGUAGE ExistentialQuantification #-}

data Bar = forall a. (Show a) => Bar a

instance Show Bar where
show (Bar a) = "Bar " ++ show a

This says that a "Bar" contains a value of type a, plus a dictionary
proving that a is of class show. The terminology is confusing,
because the term Existantial refers to the value (for all values of
type Bar, there exists a Show dictionary for the a). But the types
are declared using forall, making it seem like the language extension
should actually be "UniversalQuantification".

ExistantialQuantification is a fairly safe extension to use.
Control.Exception makes use of it, so the extension is probably here
to stay. However, it's not quite a drop in replacement for the Foo
example above, because the Bar type constructor does not take a type
argument. You might actually want to define some functions on, say
(Foo Int), so that they only work on int, and other functions on (Foo
a) for any a in the Show class. There is another less safe extension
called GADTs that lets you do that.

The basic idea with GADTs is that you define your constructors by
declaring their function types. For example:

{-# LANGUAGE GADTs #-}

data Baz a where
BazConstructor :: (Show a) => a -> Baz a

showBaz :: Baz a -> String
showBaz (BazConstructor a) = show a -- okay

(I used BazConstructor just to make clear where the constructor is,
but you could just as easily also call it Baz.) In this case, a Baz
using the BazConstructor includes a dictionary, so it is possible to
call show a even without a (Show a) constraint on the showBaz
function.

In addition to the fact that they are less well excepted, there are a
couple of other gotchas with GADTs. One is that enabling GADTs makes
all let bindings that would require ad-hoc polymorphism monomorphic
(unless you declare a type in the let binding). This is in contrast
to normal Haskell, where the compiler infers polymorphic types for
bindings that look like functions (see the DMR slides in the second
lecture).

A second gotcha is that the record syntax is fairly unintuitive. I
actually didn't even remember, and found that it works like this:

data Baz a where
Baz :: (Show a) => { unBaz :: a } -> Baz a

However, that appears to have changed in a recent version of GHC, so
older code uses a different syntax.

David

[David Terei]

On 4 November 2011 21:22, <dm-list-clas...@scs.stanford.edu> wrote:
> In addition to the fact that they are less well excepted, there are a
> couple of other gotchas with GADTs.  One is that enabling GADTs makes
> all let bindings that would require ad-hoc polymorphism monomorphic
> (unless you declare a type in the let binding).  This is in contrast
> to normal Haskell, where the compiler infers polymorphic types for
> bindings that look like functions (see the DMR slides in the second
> lecture).

He I thought you may be wrong for a second here and so read through
and old blog post from Simon PJ,

http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

May be an interesting read for some people. 7.2 has made mono local
binds the default (regardless of GADTs) but also relaxed the feature
so that certain let bindings are generalized even when MonoLocalBinds
is on.

Cheers,
David

[dm-list-clas...@scs.stanford.edu]

At Sat, 5 Nov 2011 13:26:46 -0700,

David Terei wrote:
>
> On 4 November 2011 21:22, <dm-list-clas...@scs.stanford.edu> wrote:

> > In addition to the fact that they are less well [accepted], there are a

> > couple of other gotchas with GADTs.  One is that enabling GADTs makes
> > all let bindings that would require ad-hoc polymorphism monomorphic
> > (unless you declare a type in the let binding).  This is in contrast
> > to normal Haskell, where the compiler infers polymorphic types for
> > bindings that look like functions (see the DMR slides in the second
> > lecture).
>
> He I thought you may be wrong for a second here and so read through
> and old blog post from Simon PJ,
>
> http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

Hmm... It does appear the situation is even more extreme than I
thought. With MonoLocalBinds, the compiler does not even generalize
parametric polymorphic types, let alone ad hoc ones.

> May be an interesting read for some people. 7.2 has made mono local
> binds the default (regardless of GADTs) but also relaxed the feature
> so that certain let bindings are generalized even when MonoLocalBinds
> is on.

I don't have GHC 7.2 handy to test on, but doesn't enabling
MonoLocalBinds by default constitute a rather serious departure from
haskell 2010? Is -XNoMonoLocalBinds really required to get Haskell
2010 semantics?

David

[David Terei]

On 5 November 2011 15:08, <dm-list-clas...@scs.stanford.edu> wrote:
>> May be an interesting read for some people. 7.2 has made mono local
>> binds the default (regardless of GADTs) but also relaxed the feature
>> so that certain let bindings are generalized even when MonoLocalBinds
>> is on.
>
> I don't have GHC 7.2 handy to test on, but doesn't enabling
> MonoLocalBinds by default constitute a rather serious departure from
> haskell 2010?  Is -XNoMonoLocalBinds really required to get Haskell
> 2010 semantics?

Setting '-XHaskell2010' is require to get Haskell 2010 semantics. The
default mode GHC uses differs slightly from this. Hmm looking through
the code for GHC just now though it doesn't appear MonoLocalBinds is
actually turned on by default. We can play around next time at the
office and see whats the current settings actually are.