Typeclass behavior in Haskell

Question

As a beginner to Haskell I'm having a hard time understanding why this is failing

-- this works fine of course
f :: Float
f = 1.0

f :: Num a => a
f = 1.0
-- Could not deduce (Fractional a) arising from the literal ‘1.0’
--      from the context: Num a
--        bound by the type signature for:
--                   f :: forall a. Num a => a

My confusion stems from them both having instances of Num. So since Int's, Integers, Doubles, etc all have an instance of the Num typeclass, why can't I stuff any numerical value in f?

For example, negate which has a signature negate :: Num a => a -> a will work with Int's Float's Doubles, etc.

Any insight would be greatly appreciated.

Answer 1

The issue here is that when you write f :: Num a => a, this means that f must work for all possible instantiations of a such that a Num a instance exists. In particular, this means that writing (f :: Int) somewhere else should work fine, since instance Num Int certainly exists. However, the value that you wrote for f to return is 1.0, which is not an integer: 1.0 :: Fractional p => p. The error message is basically saying that "Knowing that a is a Num doesn't tell us that a is a Fractional, so there's no way for the fractional literal 1.0 to have type a".

One way to think about it is that the caller gets to choose what a should be: this is why type signatures of this form are called universally quantified.

You may be thinking of existential quantification: f returns some kind of Num, but the "caller" doesn't know what Num was returned. This is often not as useful as universal quantification, and is a little clunky in Haskell, but can be done like this:

{-# LANGUAGE ExistentialQuantification #-} -- This is a GHC extension
-- A SomeNum value contains some kind of Num. Can't see what kind from the "outside".
data SomeNum = forall a. Num a => SomeNum a
f :: SomeNum
f = SomeNum 5.0

In Haskell, a signature like f :: a is syntax for the (conceptually clearer) f :: forall a. a, where the forall is a lot like a "type-level lambda" (and not the f :: exists a. a which you may have been thinking of). In fact, if you look at GHC Core, you will see that all these type applications are explicit: whenever you use a universally quantified function, the "caller" explicitly passes in the types to use for each of the type variables.

However, I would advise that you not try to use existential quantification at this stage: there are often better/easier alternatives. I just wanted to explain it to help show the difference between existentials and universals.

Answer 2

why can't I stuff any numerical value in f?

For example, negate which has a signature negate :: Num a => a -> a will work with Int's Float's Doubles, etc.

Precisely because of that!

You can't stuff any numerical value in the definition of f, as you can't stuff any numerical value in the definition of negate.

Suppose we tried to define negate as follows

negate :: Num a => a -> a
negate x = 10.5 - 10.5 - x

Would that work on an Int? That is, on negate 42 :: Int? No, since 10.5 is not an Int.

Since the type of negate promises that it works on any numeric type, including Int, but it does not actually work on Int, then the promise is broken. Static type checking rejects that code because of this.

Similarly, if type checking accepted

f :: Num a => a
f = 10.5

then all of these should work: f + 8 :: Int, f / 2 :: Double, f - 4 :: Integer. But 10.5 does not fit into Int (nor into Integer).

The issue here is that f :: Num a => a allows the caller to choose any numeric type a. Since the type allows the caller to choose, f can not choose itself, but must adapt to any choice made by the caller. So, f can not use code which only works at some numeric types, but not others.

If f only works at Fractional types, a subset of Num types, then the type of f must advertise to the caller that its choice is limited to fractional types. This is done by using f :: Fractional a => a instead.