Adding type constraints to data declarations

Question

I've been reading about making our own types and type classes from Learn You a Haskell for Great Good. I don't quite understand the behaviour of the Haskell compiler when I add a type constraint to my data declarations.

For example, I have

{-# LANGUAGE DatatypeContexts #-}

data (Ord a) => OrderedValue a = OrderedValue a

getOrderedValue :: OrderedValue a -> a
getOrderedValue (OrderedValue a) = a

As can be seen above, I have a type constraint on my data declaration, stating that any value that is contained inside an OrderedValue must have an Ord instance.

I tried compiling this code and the compiler spit out

• No instance for (Ord a) arising from a use of ‘OrderedValue’
  Possible fix:
    add (Ord a) to the context of
      the type signature for:
        getOrderedValue :: forall a. OrderedValue a -> a
• In the pattern: OrderedValue a
  In an equation for ‘getOrderedValue’:
      getOrderedValue (OrderedValue a) = a

Changing the definition of getOrderedValue to

getOrderedValue :: (Ord a) => OrderedValue a -> a
getOrderedValue (OrderedValue a) = a

expectedly fixed the problem.

My question is - why is the compiler complaining here? I assumed the compiler should be able to infer that the a being pattern matched in

getOrderedValue (OrderedValue a) = a

has an Ord instance, because the OrderedValue value constructor is for constructing instances of type OrderedValue that has a type parameter a that has an Ord instance.

Phew, that was a mouthful.

Thanks.

EDIT - I had a look at the alternate answers that @melpomene suggested, thanks for that. However, I'm looking for an answer that describes why the Haskell language designers chose to implement it this way.

Possible duplicate of Why does Haskell stop short of inferring the datatype's typeclasses in the function signatures? — melpomene
Ideed the compiler can infer it: try to remove the function type signature and see. But here you are disabling any inference because you are explicitly giving a type to your function, so the compiler does not even start inferring. It just complains the signature is wrong (or rather that the function is wrong for that signature) — gigabytes
@diveshpremdeep It shouldn't be surprising that adding a function signature can change the behaviour of the compiler. If you add a signature that's just wrong, like sort :: IO Double -> Char, then this surely must cause a compile-time error. The point is that you can ask the compiler what the (most general) correct signature is, rather than writing it yourself – though more often it actually works better to start with the signature and let the compiler help you with the implementation instead. And, sometimes signatures are actually needed, in particular when Rank-2 types are involved. — leftaroundabout
As @leftaroundabout said, this is just a case of a wrong type signature. If you write the same type signature that the compiler would have inferred alone, of course he behaviour does not change. But if you write a wrong one, or one correct but less general than the most general one (which is the one inferred), then of course the compiler acts accordingly. — gigabytes
@diveshpremdeep Type-inference is undecidable in any relatively complex type system. The Haskell compiler needs type signatures in many situations. Regarding your code: I hope you have read the book: you should not add such constraints on a data declaration. They really add nothing to your type and only cause headaches. There are better alternatives. — Bakuriu

gigabytes gigabytes · Accepted Answer · 2018-10-21T07:25:52

Ideed the compiler can infer it: try to remove the function type signature and see. For example, with ghci:

Prelude> :set -XDatatypeContexts
Prelude> data Ord a => OrderedValue a = OrderedValue a
Prelude> let getOrderedValue (OrderedValue a) = a
Prelude> :t getOrderedValue
getOrderedValue :: Ord t => OrderedValue t -> t

However, by explicitly stating a type for your function, you are disabling any inference. Type inference kicks in when there is no explicit type annotation for a term. If you explicitly give it, that is the type the term will have no matter what, so it has to be correct.

So, the compiler here is type-checking your code, and finds that a type such as OrderedValue a -> a is wrong, because it ignores the Ord a constraint.

However, note that DatatypeContexts, which allows you to put the constraint on the data type, is deprecated. The consensus about it is that it is better to put constraints only on the functions that really need them. If you remove the Ord a constraint from the data type, then the getOrderedValue function compiles well, because there would be no Ord a constraint to obey, and indeed you can notice that this matches more closely the intuition behind the original type you wrote, which now is correct.

As an aside, note that the type that the compiler infers automatically is the most general one for the particular body of the function to correctly type-check, but you can explicitly give a less general type.

For example, the following function:

mysum = foldr (+) 0

has type (Num b, Foldable t) => t b -> b, but you can write:

mysum :: [Integer] -> Integer
mysum = foldr (+) 0

because that's a correct type for the function, albeit a more specific one. Of course, then once the specific type is assigned to mysum, you cannot call it with another instance of Foldable or another Num type: you loose the generality when you specialize the type.

Adding type constraints to data declarations

1 Answers