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:

Click to copy

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

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

Click to copy

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:

Click to copy

fix add :: Integer -> Integer -> Integer

And it seems to work like I'd expect:

Click to copy

> (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.