Simplify Haskell Type Signatures

Question

My question is about how to work with Haskell type signatures analytically. To make it concrete, I'm looking at the "fix" function:

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

and a little made-up function that I wrote to do Peano-ish addition:

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

When I examine the types, I get my expected type for fix add:

fix add :: Integer -> Integer -> Integer

And it seems to work like I'd expect:

> (fix add) 1 1
2

How can I work with the type signatures for fix and for add to show that fix add has the above signature? What are the "algebraic", if that's even the right word, rules for working with type signatures? How could I "show my work"?

Answer 1

ghci tells us

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

modulo some typeclass noise since the second argument to add requires an Eq instance (you're checking it 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, the as in fix :: (a -> a) -> a can have any type. In this case they have type (a -> a -> a)

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

You can work with Haskell's type signatures in a very algebraic fashion, variable substitution works just like you'd expect. In fact, theres a direct translation between types and algebra.