Why does (Ord a Num b) => a -> b -> a result in (Ord a, Num a) -> a

I’m working on an exercise from Haskell First Principals and not understanding the following.

I have the type

kessel :: (Ord a, Num b) => a -> b -> a; kessel = undefined

And

> :t kessel 1 2

gives: kessel 1 2 :: (Ord a, Num a) => a

So b is removed from the type signature and it says, as I understand it, a must be both Ord & Num, but the original signature seemed to say that both a & b can be different types. Did it just remove b because I passed it two params of the same type or is there something else to it?

But I can give kessel a string and an int

:t kessel "ca" 1

which gives: kessel "ca" 1 :: [Char].

String (“ca”) has the type class Ord so it takes that, and the original signature says it returns a, so the type of the first parameter. However, I don’t know why kessel "ca" 1 :: [Char] has no type constraints.

I’m guessing I am unaware of some guiding generalization or rule on how types work. Was hoping someone could shed some light for me.

If you apply an argument to a function then one argument in the type logically also disappears.

So if you start with

kessel :: (Ord a, Num b) => a -> b -> a

and you apply 1 :: Num a => a then you get

kessel 1 :: (Ord a, Num a, Num b) => b -> a

(the extra Num a constraint is because the literal 1 has that constraint and the type of the first argument must be equal to the type of the result, so that result also must have a Num instance)
if you then further apply 2 :: Num a => a then you get

kessel 1 2 :: (Ord a, Num a) => a

If you apply "ca" :: String (which has an Ord instance) then you get

kessel "ca" :: Num b => b -> String

(note that the second a also becomes String now). And then finally you can apply 1 :: Num a => a which makes the final type

kessel "ca" 1 :: String

Normally you would get an error about ambiguous types, because you only specify that the b is a Num and not a concrete type, but Haskell uses defaulting rules for Num, which always chooses Integer if I remember correctly.

5 Likes

Thanks for you reply. After going through it, here is how I modified my understanding. It is a bit long so understandable if you can’t reply to all of it.


kessel

I’d like to confirm that is the ‘compiler’ that is the type magic below so I don’t say it the wrong way?

1. :t kessel 1 2

(Ord a, Num b) => a -> b -> a – original

(Ord a, Num a) => a – result

  • Since both a & b are Num a separate type for b is not needed to express the type so the compiler eliminates it.
  • I’m curious what the first parameter was passed a Num, why it is Ord & not Num?

2. :t kessel "ca" 1

(Ord a, Num b) => a -> b -> a – original

[char]

Similar to #1 above, two parameters are passed but in this case no parameter types are included. I.e., I was expecting something like:

(some param types here) => [char]

  • For some reason it seems the type constraints are not needed?

3. :t kessel "ca"

(Ord a, Num b) => a -> b -> a – original

Num b => b -> [ Char ]

I think I get this one:
a was given a [Char] and is not gone. The return type is [Char] because the original signature says it will match a, and the function is waiting for b which must be a Num.

4. :t kessel 1

(Ord a, Num b) => a -> b -> a – original

(Ord a, Num b, Num a) => b -> a

My understanding here is:

a was passed as a Num so the return type must be a Num and this constraint has been added as the last Num a.

  • Instead of saying ‘the return type …’ is it also true OK to think about it as Num a was added because the compiler was given addition information (i.e., 1) about a and adds that new info to the type constraints?

I’m going to throw out a totally not valid pseudo-syntax to see if it clears up any of the concepts. You can kind of imagine that kessel would have type
(Ord a => a) -> (Num b => b) -> (Ord a => a). Now of course we actually put all the constraints first (and don’t duplicate them), but it might help to think about the constraints following the data around instead of following the function around.

Let’s actually take case # 2 first, since that’s the simplest: kessel "ca" 1
So we give it “ca” for our Ord a => a (which specializes a to be a [Char]), and we also pass in 1 for our Num b => b (which specializes b to be an Integer, because there’s some special rules where Num defaults to Integer like @jaror said) so after applying both arguments, you’re left with just Ord a => a, but we already specialized that to [Char], so we just return a [Char]. There are no constraints left on the [Char] value - indeed at this point it’s a concrete type so there would be no meaning to a constraint - it’s exactly [Char] and no other orderable or numeric thing.

So for 1, kessel 1 2: This time we give it 1 for our Ord a => a. Number literals like 1 are special because all it means is that it has a Num constraint, but it still could be many different types at runtime. It’ll default to Integer if it has to settle on something, but it’ll only do that at the last possible moment. Num also doesn’t imply Ord, so we still keep our Ord from the kessel signature, and now we’re adding a Num constraint. Our first argument then becomes a (Ord a, Num a) => a, and since our first argument is this (Ord a, Num a) => a and our return value has to be the same type as the first argument, that’s what we’re left with. Everything about b has already been handled just like in the previous example.

Everything you wrote about example #3 is spot on.

#4 is just like #1 except we haven’t done anything with b yet so the Num b => b sticks around. We could use our invalid pseudo syntax to say
(kessel 1) :: (Num b => b) -> ((Ord a, Num a) => a)

Instead of saying ‘the return type …’ is it also true OK to think about it as Num a was added because the compiler was given addition information (i.e., 1) about a and adds that new info to the type constraints?

Yep, I think that’s a good way to think about it.

Did that make any sense?

1 Like

@ntwilson Yes, it made sense and I think I’m about 90% there on this now, which is enough to move ahead. Thanks!

1 Like

Hi klequis,

The other explanations cover what is happening very well but I wanted to say one thing specifically about

“Did it just remove b because I passed it two params of the same type or is there something else to it?”

that I think might also help because I think it can be explained in a lot more simple terms.

The reason that it ‘removed’ b is because you applied the function to the b argument already. As another example, consider

:t even
even :: Integral a => a -> Bool

:t 1
1 :: Num p => p

:t even 1
even 1 :: Bool

The a is removed from the expression “even 1” because you have already applied an argument to the function. The type of “even 1” is the type that the function returns when it is passed an argument that has the type 1 has, so the argument types are removed because we are dealing with a function that has already been applied to the right number of arguments. If “even 1” had the type “Integral a => a -> Bool” then that would mean it is still a function that is waiting for one argument and will return a Bool if it is given a type that is in the Integral class. Which would then imply that “even” itself is a function with two arguments. But that is clearly not the case.

This fundamentally has to do with currying. If you have a function that takes multiple arguments and you supply it with some of the arguments, you will get back a function that is waiting for the rest of the arguments, and none of the previous arguments will be mentioned because they’ve already been applied. The types, like the first a and the b in your kessel example, will be removed because they’ve already been applied. If you supply all of the arguments, then the type will just be the return type of the function, and of course that type can be constrained in different ways depending on what arguments you gave it.

As I said, the other comments did a very good job of explaining what is happening with the constraints. I just wanted to point this part out because I don’t think it was explicitly mentioned before and it seems like from your original question that this might also be a confusion point. Hopefully this helps clear up the last 10% of your confusion.

1 Like

Thank you for that KripkesBeard. I see now that I was so caught-up in the details of types and the addition of type constraints that I missed the basics of currying.

I think I’m also getting that when you take

kessel :: (Ord a, Num b) => a -> b -> a; kessel = undefined

and you call it with

kessel "ca"

you get

kessel "ca" :: Num b => b -> [Char]

Where the Ord constraint is gone not only because the function has already been applied to a but also because the remaining param is of type Num and Num always includes Ord, so Num a implies Ord. Am I getting that right?

Heh, you would think so, but actually not. Num has no superclass nor laws associated with it, only suggestions for how a Num should behave. I initially thought that Num implied Ord too.
No, the reason that Ord went away is because it was on type a. Type b was never constrained to be Ord. You had some variable type a (or “generic” in many other languages) that was constrained that a had to be an instance of the Ord class. But as soon as you apply "ca", you’re effectively saying that a must be [Char]. a can’t be anything else anymore. You don’t need to bother saying that a has to be an Ord thing, because a is actually just [Char]. In fact all mention of a disappears from the signature because if you used any other type for a besides [Char] at this point, it wouldn’t type check. Also, we already know that [Char] is an Ord thing without having to write that out as a constraint.

Here’s another example of the same thing: In GHCi, I can say

> import qualified Data.Map as Map
> :t Map.lookup
Map.lookup :: Ord k => k -> Map k a -> Maybe a
> :t Map.lookup "hi"
Map.lookup "hi" :: Map [Char] a -> Maybe a

Notice that in just Map.lookup, the key could be any variable type k so long as k was an Ord. But as soon as I apply the first argument, I specialize (“lock in”) k as [Char], and suddenly all mention of k and Ord k disappear. They just get replaced by [Char], which is known to be Ord already. And of course I get a compiler error if I try to make a non-Ord k:

> :t Map.lookup (id :: Int -> Int)
error:
    * No instance for (Ord (Int -> Int))
        arising from a use of `Data.Map.lookup'
        (maybe you haven't applied a function to enough arguments?)
    * In the expression: Data.Map.lookup (id :: Int -> Int)
      In an equation for `it': it = Data.Map.lookup (id :: Int -> Int)
1 Like

Thanks for the clarification! I now see that > :i Num makes that fact clear.