Simplify Haskell Type Signatures

Question

My question is how to analyze work with signatures like Haskell. To make this specific, I look at the "fix" function:

fix :: (a -> a) -> a 

and a little created function that I wrote to make the addition of Peano-ish:

 add = \rec ab -> if a == 0 then b else rec (a-1) (b+1) 

When I look at types, I get the expected type for fix add :

 fix add :: Integer -> Integer -> Integer 

And it works as I expected:

 > (fix add) 1 1 2 

How can I work with type signatures for fix and add to show that fix add has the specified signature? What is “algebraic”, even if it is the right word, the rules for working with the type of signatures? How can I "show my work"?

Answer 1

ghci tells us

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

modulo is some class type noise, since the second argument add requires an instance of Eq (you check for equality with 0 )

When we apply fix to add , the signature for fix becomes

fix :: ((a -> a -> a) -> (a -> a -> a)) -> (a -> a -> a)

Remember that a in fix :: (a -> a) -> a can be of any type. In this case, they are of type (a -> a -> a)

So fix add :: Num a => a -> a -> a , which is exactly the right type to add two a s.

You can work with signatures like Haskell very algebraically; variable substitution works just as you expected. In fact, theres a direct translation between types and algebra.