Type signature confusion-CodePudding

So I have this function in my code

type Player = Char

choose :: Player -> a -> a -> a
choose p a b
  | p == 'X' = a
  | p == 'O' = b

At one point it is used like so

(choose p ( ) (-)) 5 5

I can clearly see that it chooses between the ( ) or (-) function and then applies it on 5 and 5. In fact I even tested it in GHCi for myself.

However, here are the type signatures for the aforementioned functions

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

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

I simply do not understand how a function of this type signature can be passed to choose. Shouldn't choose have a type signature like this?

choose :: Num a => Player -> (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a)

Could someone help me shine a light on this?

CodePudding user response：

Those are not the same a.

The a is signature for choose is not the same a as in signature for ( ) and (-). They happen to have the same name, but they're separate type variables, not related to each other at all.

So, to clear up the confusion, let's rename one of them:

choose :: Player -> x -> x -> x
(-) :: Num a => a -> a -> a
( ) :: Num a => a -> a -> a

Now, if we apply choose p ( ) (-), that checks out just fine if we set x ~ (a -> a -> a)

CodePudding user response：

You need to remember that type variables can be instantiated on each use, and can be instantiated to complicated types that themselves have multiple parts! A function type like a -> a -> a is just as good a type to substitute for type variables as is Int, or [Char], or (Double, Double), etc.

So if we instantiate the a type variable to Char we get this:

-- here choose is used as Player -> Char -> Char -> Char
choose p 'X' 'O'

And if we instantiate the a type variable to a -> a -> a, then we get this:

-- here choose is used as Num a => Player -> (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a)
choose p ( ) (-)

So anytime you see a function's type taking an argument or returning a result that is a simple type variable, like id :: a -> a, that does not mean you can't apply it to functions! Much more complicated-looking things like (t -> Int -> [t]) -> (t -> Int -> [t]) are particular examples of the full generality of what you can use a simple type like a -> a for.

You need to learn to see function types as not particularly special; they are just one of many kinds of types that exist, and anything that claims to work for all types must work for function types too.

Also remember that type variables in two different type signatures are in different scopes. The variable a in the original choose :: Player -> a -> a -> a is not the same variable a in ( ) :: Num a => a -> a -> a or even the one in choose :: Num a => Player -> (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a). If it helps, while you're working things out you can always rename variables across all of the type signatures you're considering (and then optionally rename the variables in the final one to match an external source like GHC). For example I could avoid confusion by saying that I'm considering ( ) :: Num b => b -> b -> b, and then substituting that for a in Player -> a -> a -> a to get Num b => Player -> (b -> b -> b) -> (b -> b -> b) -> (b -> b -> b).