Haskell weird expression

Question

I would like to understand why the following is a valid expression in Haskell:

Prelude> let e = (+) (-)
Prelude> :type e
e :: (Num (a -> a -> a), Num a) => (a -> a -> a) -> a -> a -> a

More strange is that any expression in the form

e 1 2 3 4 ... N

whatever N are all valid expressions of uncomprehensible type. For example,

Prelude> :t e 1 2 3 4 5
e 1 2 3 4 5
  :: (Num ((a -> a1 -> t) -> (a -> a1 -> t) -> a -> a1 -> t),
      Num (a -> a1 -> t), Num a1, Num a) =>
     t

Is this an unfortunate consequence of currying and type inference?

Clarifications are welcome.

Answer 1

It's not an "unfortunate consequence". In fact, some might see it as a feature! The types of (+) and (-) are

> :t (+)
(+) :: Num a => a -> a -> a
> :t (-)
(-) :: Num a => a -> a -> a

It's important to realize that this is valid for any type a, even if a is a function type. So, for example, if the type b -> b -> b has a Num instance, then you could restrict (+) to

(+) :: Num (b -> b -> b) => (b -> b -> b) -> (b -> b -> b) -> b -> b -> b

by simply setting a = b -> b -> b. Because of currying, the parentheses around the last three bs are unnecessary (you could write them in but they would be redundant).

Now, Num b => b -> b -> b is exactly the type of (-) (with the proviso that b itself has to have a Num instance), so the function (-) fills the first "slot" of (+) and the type of (+) (-) is

(+) (-) :: (Num b, Num (b -> b -> b)) -> (b -> b -> b) -> b -> b -> b

which is what you observed.

---

This raises the question of why on earth it might be useful to have a Num instance for functions at all. In fact, does it even make sense to define a Num instance for functions?

I claim that it does! You can define

instance Num a => Num (r -> a) where
    (f + g) r = f r + g r
    (f - g) r = f r - g r
    (f * g) r = f r * g r
    abs f r = abs (f r)
    signum f r  = signum (f r) 
    fromInteger n r = fromInteger n

which makes perfect sense as a Num instance. And in fact, this is precisely the instance you need to interpret your expression e -

> let e = (+) (-)
> e 3 2 1
4

Buh?!?

What happened is the following. Since (Num a) => r -> a is a valid Num instance for any r, you can replace r with a -> a, which shows that (Num a) => a -> a -> a is also a valid Num instance. So you have

-- Remember that (+) f = \g r -> f r + g r

  (+) (-) 3 2 1
= (\g r s -> (-) r s + g r s) 3 2 1 -- definition of (+) on functions
= (\  r s -> (-) r s + 3 r s) 2 1   -- beta reduction
= (\    s -> (-) 2 s + 3 2 s) 1     -- beta reduction
=            (-) 2 1 + 3 2 1        -- beta reduction
=            (2 - 1) + 3            -- since (3 2) = 3 and (3 1) = 3
=               1    + 3
=               4

A little convoluted (in particular, make sure you understand why 3 2 = 3) but not too confusing once you've expanded all the definitions out!

---

You asked for the derivation of the type of (+) (-) that Haskell uses. It relies on the idea of "unification" of type variables. It goes something like this -

1. You know that (+) :: Num a => a -> a -> a and (-) :: Num b => b -> b -> b (I use different letters because we will want to mash these together).
2. If you are going to put (-) into the first slot of (+) you must have a ~ b -> b -> b, so the combined type is
3. (+) (-) :: (Num a, Num b, a ~ b -> b -> b) => (b -> b -> b) -> (b -> b -> b)
4. Now you "unify" a with b -> b -> b (as indicated on the left of the fat arrow, by the ~ sign) which leaves you with
5. (+) (-) :: (Num (b -> b -> b), Num b) => (b -> b -> b) -> (b -> b -> b)
6. If we remove the right-most parentheses (because they are redundant) and rename b to a, this is the type signature that Haskell infers.