Determining the type of a function in Functional Programming

Question

The following equations are written in Miranda Syntax, but due to the similarities between Miranda and Haskell I expect Haskell programmers should understand it!

If you define the following functions:

rc v g i = g (v:i)
rn x = x
rh g = hd (g [])


f [] y = y 
f (x:xs) y = f xs (rc x y)

g [] y = y
g (x:xs) y = g xs (x:y)

How do you work out the type of the functions? I think I understand how to work it out for f,g and rn but I'm confused about the partial application part.

rn is going to be * -> * (or anything -> anything, I think it's a -> a in Haskell?)

For f and g, are the function types both [*] -> * -> *?

I'm unsure how to approach finding the types for rc and rh though. In rc, g is being partially applied to the variable i - so I'm guessing that this constrains the type of i to be [*]. What order are rc and g applied in the definition of rc? Is g applied to i, and then the resulting function used as the argument for rc? Or does rc take 3 separate parameters of v,g and i? I'm really confused.. any help would be appreciated! Thanks guys.

Sorry forgot to add that hd is the standard head function for a list and is defined as:

hd :: [*] -> *
hd (a:x) = a
hd [] = error "hd []"

Answer 1

The type is inferred from what is already known of types and how expressions are used in the definition.

Let's begin at the top,

rc v g i = g (v : i)

so rc :: a -> b -> c -> d and we must see what can be found out about a, b, c and d. On the right hand side, there appears (v : i), so with v :: a, we see that i :: [a], c = [a]. Then g is applied to v : i, so g :: [a] -> d, altogether,

rc :: a -> ([a] -> d) -> [a] -> d

rn x = x means that there's no constraint on the argument type of rn and its return type is the same, rn :: a -> a.

rh g = hd (g [])

Since rh's argument g is applied to an empty list on the RHS, it must have type [a] -> b, possibly more information about a or b follows. Indeed, g [] is the argument of hd on the RHS, so g [] :: [c] and g :: [a] -> [c], hence

rh :: ([a] -> [c]) -> c

Next

f [] y = y 
f (x:xs) y = f xs (rc x y)

The first argument is a list, and if that is empty, the result is the second argument, so f :: [a] -> b -> b follows from the first equation. Now, in the second equation, on the RHS, the second argument to f is rc x y, hence rc x y must have the same type as y, we called that b. But

rc :: a -> ([a] -> d) -> [a] -> d

, so b = [a] -> d. Hence

f :: [a] -> ([a] -> d) -> [a] -> d

Finally

g [] y = y
g (x:xs) y = g xs (x:y)

from the first equation we deduce g :: [a] -> b -> b. From the second, we deduce b = [a], since we take the head of g's first argument and cons it to the second, thus

g :: [a] -> [a] -> [a]