2

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.

divesh premdeep
  • 1,070
  • 3
  • 16
  • 28
  • 1
    Possible duplicate of [Why does Haskell stop short of inferring the datatype's typeclasses in the function signatures?](https://stackoverflow.com/questions/2170341/why-does-haskell-stop-short-of-inferring-the-datatypes-typeclasses-in-the-funct) – melpomene Oct 17 '18 at 07:10
  • 1
    ... or https://stackoverflow.com/questions/12770278/typeclass-constraints-on-data-declarations – melpomene Oct 17 '18 at 07:10
  • 2
    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 Oct 17 '18 at 07:18
  • @gigabytes This is the first occurrence I've encountered where adding a function signature actually change the behaviour of the compiler. I thought function signatures served more of a readability / documentation purpose because they are not really needed. – divesh premdeep Oct 17 '18 at 07:49
  • @melpomene Cheers, however, those answers don't explain the "why" aspect of it. – divesh premdeep Oct 17 '18 at 07:58
  • 3
    @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 Oct 17 '18 at 08:01
  • 3
    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 Oct 17 '18 at 09:18
  • 1
    Signature are for documentation purposes, but not only for that. Regular documentation is human-only. Signatures, instead, are read by both humans and the compiler, which will check the code against the signature. Indeed, we add them in the code so that the compiler can point out errors as early as possible. If we want a function to return a string, but we make a mistake and make it return boolean, the compiler would happily infer the unintended type, and report errors (perhaps) only when the function is used, surprising the programmer. With a type signature the error is found early. – chi Oct 17 '18 at 09:28
  • 2
    @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 Oct 17 '18 at 21:07
  • @gigabytes Indeed, if I omit the type declaration, the compiler happily compiles my code. As I understand it, my original code fails because I'm overriding the compiler's inferred type declaration with my own, which user leftaroundabout has mentioned. Please add your comment as an answer so that I can accept it. Thanks! – divesh premdeep Oct 18 '18 at 03:31
  • @Bakuriu I am going through the book right now. I was simply curious about why the compiler behaves this way. – divesh premdeep Oct 18 '18 at 03:42
  • see [this answer](https://stackoverflow.com/a/2172085/849891) at the first proposed duplicate. – Will Ness Oct 21 '18 at 15:13

1 Answers1

4

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.

gigabytes
  • 3,104
  • 19
  • 35