Enforce class constraints in type class that is not captured in the type signature of implementing type

Question

I am trying to use a typeclass that enforces a constraint on the type returned by one of the functions it defines. But the return type of the function does not capture the constraint in its type variable. I would like to know what is wrong with the code or what is the correct way to encode it. A sample code is given below:

  data State a = State {
    uniform :: a
  }
  class Renderable a where
    render :: (Uniform b) => Int -> a -> State b

  library :: (Uniform a) => a -> IO ()
  -- some implementation

  draw :: (Renderable a) => a -> IO ()
  draw renderable = do
    let state = render 0 renderable
    _ <- library (uniform state)

In the above snippet, the render function tries to enforce that the uniform property in State adheres to a class constraint Uniform. When I run the code, I am getting an error that

 Could not deduce (Uniform a5) arising from a use of ‘draw’
  from the context: (Renderable r, Uniform a)
  bound by the type signature for:
               draw :: forall r a.
                       (Renderable r, Uniform a) =>
                       Int -> Renderable r -> IO ()

Thinking of it, I am sort of able to understand that since the type of draw uses only Renderable and Renderable does not have a parameter of type Uniform in its type signature, the compiler is not able to verify the flow completely. But I am wondering, why cant the compiler, while testing the type signature of draw ignore the issue and basically depend on the fact that it will know if a type implementing Renderable will definitely have to provide a value for uniform as a part of State and it can verify the type correctness in the implementation site rather than usage.

PS: This is an extracted snippet from OpenGL code and Uniform, Library are opengl terminologies.

Answer 1

Here is a technique for you. I've written about this many years ago (in a slightly different context, but the idea is the same) and I still stand by it.

First, the framing. If we write out the signature of render explicitly, we have:

render :: forall b. Uniform b => Int -> a -> State b

That is, the caller of render chooses the type b. It seems to me that your intention is more like this pseudo-Haskell*:

render :: exists b. (Uniform b) & Int -> a -> State b

In which the callee gets to choose the type. That is, different implementations of render may choose different types b to return, so long as they are uniform.

This might be a fine way to phrase it, except that Haskell does not support existential quantification directly. You can make a wrapper data type to simulate it

data SomeUniform where
    SomeUniform :: Uniform a => a -> SomeUniform

making your signature

render :: Int -> a -> SomeUniform

which I think has the properties you are looking for. However the SomeUniform type and the Uniform typeclass are very likely superfluous. You said in the comments that the Uniform typeclass looks like this:

class Uniform a where
    library :: a -> IO ()

Let's consider this question: let's say we have a SomeUniform, that is, we have a value of some type a about which we know nothing except that it is an instance of the Uniform typeclass. What can we possibly do with x? There is only one way to get any information out of x, and that is to call library on it. So in essence the only thing the SomeUniform type is doing is carrying around a library method to be called later. This whole existential/typeclass is kind of pointless, we would be better served collapsing it down to a simple data type:

data Uniform = Uniform { library :: IO () }

and your render method becomes:

render :: Int -> a -> Uniform

It's so beautifully unfancy, isn't it? If there were more methods in Uniform typeclass, they would become additional fields of this data type (whose types may be functions, which can take some getting used to). Where you had types and instances of the typeclass, e.g.

data Thingy = Thingy String
-- note the constructor type Thingy :: String -> Thingy

instance Uniform String where
    library (Thingy s) = putStrLn $ "thingy " ++ s

you can now also be rid of the data type and just use a function in place of the constructor

thingy :: String -> Uniform
thingy s = Uniform { library = putStrLn $ "thingy " ++ s }

(If you can't get rid of the data type for other reasons, you can provide a conversion function instead uniformThingy :: Thingy -> Uniform)

The principle here is, you may replace an existential type with the collection of its observations, and it's usually pretty nice if you do.

---

* My pseudo-Haskell & is dual to =>, playing essentially the same role but for existentially quantified dictionaries. c => t means that once the caller provides the dictionary c, the type t is returned, whereas c & t means that the callee provides both the dictionary c and the type t.

Answer 2

It appears that you're expecting to be able to define render to return a different distinct type for each implementation of Renderable, as long as that type is Uniform:

instance Renderable Foo where
  render _ _ = State True

instance Renderable Bar where
  render _ _ = State "mothman"

instance Renderable Baz where
  render _ _ = State 19

So if render is called with a Foo, it will return a State Bool, but if it's called with a Bar it will return a State String (assuming both Bool and String are Uniform). This is not how it works, and you'll get a type mismatch error if you try instantiating like this.

render :: (Uniform b) => Int -> a -> State b means that a Uniform b => State b is returned. If this is what your type signature is, your implementation must be no more or less specific; your implementation must be able to return a value of ANY type Uniform b => State b. If it is not able to do so, any code that requests a return value of a specific type won't get the right type, and things will break in ways that the type system SHOULD be able to prevent.

Let's look at a different example:

class Collection t where
  size :: Num i => t a -> i

Assume someone wants to run this size function, and get the result as a Double. They can do that, because any implementation of size must be able to return any type of class Num, so the caller can always specify which type they want. If you were allowed to write an implementation that always returned an Integer, this would no longer be possible.

---

I think to do what you're trying to do, you'd need something like FunctionalDependencies. With this, your class can be something like:

class Uniform b => Renderable a b | a -> b where
  render :: Int -> a -> State b

The "| a -> b" tells the type checker that the type b should be decided based on the type a provided by the caller. This disallows the caller from choosing their own b, which means the implementation should force a more specific type. Note that now you need to specify both a and b in your instances, so:

instance Renderable Foo Bool where ...
instance Renderable Bar String where ...

I'm certain there are other valid approaches to this problem, as well.