Haskell function type generalization-CodePudding

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]?

CodePudding user response：

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.

CodePudding user response：

The first thing to realize is that, for any equation, any variables defined in that equation, are scoped only to that equation. In particular, this means that the x on the first line is not related at all to the x on the second line. These are two separate variables, they just happen to have the same name.

Now, you have already correctly determined that y :: Bool and g :: Bool -> [Bool] -> b for some as of yet unknown b. And therefore, g y :: [Bool] -> b

The next thing to observe is that, since maybe :: p -> (q -> p) -> Maybe q -> p, which means that q ~ [Bool] (coming from the type of g y) and p ~ Int (coming from the literal 42). And therefore, g :: Bool -> [Bool] -> Int and x :: Maybe [Bool] (since it's used as the third parameter of maybe).

Finally, from the second equation, we can see that the function's return type is whatever maybe returns, which is Int. And therefore, that's also the type of the first parameter, because it's being returned in the first equation.

Taking all of that together:

f :: Int -> Maybe [Bool] -> Bool -> Int

One final stroke: I actually lied a little. The literal 42 is not really Int. Such literal can be any type that has an instance of the Num class. To account for that, let's replace our Ints in the signature with a generic type and give that type a Num constraint:

f :: Num a => a -> Maybe [Bool] -> Bool -> a