Haskell polymorphism type calculation
I need to calculate the types of the following expressions:
- curry fst
- foldr const
- (foldr const). (curry fst)
First I have:
curry :: ((a, b) -> c) -> a -> b -> c
fst :: (d, e) -> d
{} | (a,b)-> c = (d,e) -> d
{} | (a,b) = (d,e) , c = d
c -> d | (a,b) = (d,e)
c -> d , a ->d | b = e
c -> d , a ->d, b -> e | {}
then replace the result with a -> b -> c and you get d -> e -> d
Now it looks like this:
foldr :: (f -> g -> g) -> g -> [f] -> g
const :: h -> i -> h
{} | (f -> g -> g) = h -> i -> h
{} | f = h , g = i, g = h
f -> h | g = i, g = h
f -> h, g -> i | i = h
f -> h, g -> i i->h | {}
then replace the result with g -> [f] -> g and you get i -> [h] -> i
Next, I have to do
(foldr const) . (curry fst)
, but I'm not sure if these results are correct. I tried anyway but got stuck. So:
(foldr const) :: i -> [h] -> i and (curry fst) :: d -> e -> d
(.) :: (j -> k) -> (l -> j) -> l -> k
then i start with:
d = (j -> k) -> (l -> j) -> l -> k, e = d -> e -> d
e = (j -> k) -> (l -> j) -> l -> k -> e -> (j -> k) -> (l -> j) -> l -> k
but it doesn't feel right and I can't go on ... Are my first two results correct? If so, how do I solve the latter?
source to share
The first result is correct.
The calculation for the second result is correct until you make the substitution in the last step. Slightly missed. You had (using =
, not ->
as the latter builds function types and hence can cause confusion)
f = h, g = i, i = h
so substitution in g -> [f] -> g
gives
h -> [h] -> h
not i -> [h] -> i
, because although g = i
it is also the case when i = h
, so together g = h
. That is, you need to either normalize your replacement (applying each new solution to instantiate the old substitution, or expanding it by providing f = h, g = h, i = h
) or applying your replacement carefully one step at a time:
g -> [f] -> g
-- f = h
g -> [h] -> g
-- g = i
i -> [h] -> i
-- i = h
h -> [h] -> h
Now, for the last step of the calculation, you have all the parts, but you missed the path .
- the infix operator. Its first argument foldr const
, which must be of type j -> k
. Its second argument is curry fst
which type must be l -> j
. It all has a type l -> k
. So the equations you have to solve are
j -> k = h -> [h] -> h -- from the first argument
l -> j = d -> e -> d -- from the second argument
Now ->
links to the right, so the first one gives
j = h
k = [h] -> h
and the second gives
l = d
j = e -> d
The combination of the two gives
h = e -> d
so we end up with (normalized)
h = e -> d
j = e -> d
k = [e -> d] -> e -> d
l = d
and the instance l -> k
gives the type
d -> [e -> d] -> e -> d
Function takes a default d
, then a list of functions, and then an input e
: if the list of functions is empty, you get a default as the result; if the list is not empty, you get the result of applying the first function to the input.
source to share