Haskell function type generalization

Question

I am studying a Haskell course since I am total beginner. There is a task which I am not able to solve although I tried many times.

The task is to determine the most general type of following function:

f x _ False = x
f _ x y     = maybe 42 (g y) x

providing we know that g :: a -> [a] -> b

Can anyone help me? Thank you

I tried to determine y :: Bool, g :: Bool -> [Bool] -> b(?) But I am not sure what should be "x" 'cause from the first row we could say that it can be maybe 42 (g y) x but there is another "x" in the expression.

So maybe the type of the f is f :: [Bool] -> [Bool] -> Bool -> [Bool]?

Answer 1

Let us start with the most generic type possible: the function takes three parameters, and thus returns an item, so we assume first that f has type:

f :: a -> b -> c -> d

We see that the third parameter matches with False so that is a Bool, so c ~ Bool. The first clause also assigns the first parameter to x and returns x, so that means that the type a of the first parameter, and that of the return type d is the same, so a ~ d.

We know that maybe has type maybe :: f -> (e -> f) -> Maybe e -> f, and 42 is the first parameter so has type f. An integer literal can have any Num type, so we know Num f. Since the return type of maybe 42 (g y) x is also f and we know that this is also a, we know that f ~ a, so we can "specialize" maybe in this case to maybe :: Num a => a -> (e -> a) -> Maybe e -> a. The third parameter in maybe 42 (g y) x is x, this is the second parameter in the f call (not to be confused with the first clause), so we know that b ~ Maybe e.

We also see a call g y with g :: g -> [g] -> h. The type of g y should match that of the second parameter of the maybe call, so that means that e ~ [g] and a ~ h. y has type Bool in the g y call, so that means that g ~ Bool, and thus the g function has type g :: Bool -> [Bool] -> a.

Now we thus have gathered the following types and equivalences:

f :: a -> b -> c -> d
maybe :: f -> (e -> f) -> Maybe e -> f
g :: g -> [g] -> h
a ~ d
c ~ Bool
Num f
f ~ a
b ~ Maybe e
g ~ Bool
e ~ [g]
a ~ h
g ~ Bool

This thus means that f has type:

   f :: a -> b -> c -> d
-> f :: a -> b -> c -> a
-> f :: a -> b -> Bool -> a
-> f :: Num f => f -> b -> Bool -> f
-> f :: Num f => f -> Maybe e -> Bool -> f
-> f :: Num f => f -> Maybe [g] -> Bool -> f
-> f :: Num f => f -> Maybe [Bool] -> Bool -> f

Hence the most generic type is f :: Num f => f -> Maybe [Bool] -> Bool -> f, or we can rename the parameters to f :: Num a => a -> Maybe [Bool] -> Bool -> a.

We can let ghci do the work, for example with:

ghci> import Data.Maybe
ghci> :{
ghci| g :: a -> [a] -> b
ghci| g = undefined
ghci| :}
ghci> :{
ghci| f x _ False = x
ghci| f _ x y     = maybe 42 (g y) x
ghci| :}
ghci> :t f
f :: Num p => p -> Maybe [Bool] -> Bool -> p

This thus means that ghci confirms this type.