2

Im trying to infer the type of:

((.) foldr)

The type i manually infer differs from the one ghci infer. Here's what i do:

(.) :: ( b -> c) -> (a->b)->a->c foldr:: (a'->b'->b')->b'->[a']->b'

Now my first doubt. Foldr has to unify with b->c foldr has to unify with (b->c) but there are more than one way to make it happen; like

b ~ (a'->b'->b') c ~ b'->[a']->b'

or..

b ~ (a'->b'->b')b'->[a'] c ~ b'

How do i know which to take?

Doing different examples in ghci i arrived to the conclusion that haskell tries to unify types in a non greedy fashion for the first argument (This conclusion is totally experimental and can be totally wrong, maybe its the reason i arrive to a wrong type for the function, but is what i thought of the type inferences ive tried on haskell). So, assuming this is true the configuration haskell tries to unify first is:

b ~ (a'->b'->b') c ~ b'->[a']->b'

So now..

(.)foldr :: (a->b)->a->c

Substituting b and c:

 (.)foldr :: (a-> (a'->b'->b') )->a->b'->[a']->b'

Which is close enough the only problem i have are the parentheses in the expression (a'->b'->b') Why can i remove them when you cannot remove those in the original foldr, and the function is gonna be an input for foldr. Why after applying the composition functor you can use partial application? Is there a rule for that? Also i would like if someone coudl confirm or deny the "non greedy" type matching..

Improve this question

2 Answers 2

Reset to default
4

The associativity of ->

In Haskell the only type of function is a -> b, which is a function that takes an a and "returns" a b. For this reason a function type of:

a -> b -> c

is implicitly:

a -> (b -> c)

that is a function that takes an a and returns a function that takes a b and returns a c. You just have to remember that -> is right associative. This is the "mechanism" that allows currying.

Answers

How do i know which to take?

So, in your example:

foldr:: (a' -> b' -> b') -> b' -> [a'] -> b'

becomes:

foldr:: (a' -> b' -> b') -> (b' -> ([a'] -> b'))

As you can see the only way to infer a type a -> b is by assigning (a'->b'->b') to a and (b'->([a']->b')) to b.

Why can I remove them when you cannot remove those in the original foldr, and the function is gonna be an input for foldr?

Because after the function composition, the type is:

(a -> (a' -> b' -> b')) -> a -> b' -> [a'] -> b' -- ^^^^^^^^^^^^^^^^^^^^

Let's focus on the first part:

(a -> (a' -> b' -> b'))

this is, for the right associativity of ->, equal to:

(a -> (a' -> (b' -> b')))

which is also equal to:

(a -> a' -> b' -> b')

for the same associativity rule.

Why after applying the composition functor you can use partial application? Is there a rule for that?

Partial application can be always applied when you have a function taking more than 1 "argument" (or more correctly, when you have a function that returns a function).

Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

So if i understood correctly you remove the parentheses here because in this case they do not impose a constraint over the possibility of using currying here. had it been (a -> ((a' -> b') -> b')) instead of (a -> (a' -> b' -> b')) then in that case the resulting type wouldve parentheses in the form of (a' -> b') -> b' am i right?
@user3558296, The ability of using currying does not depend on how many parenthesis you place (as long as the type remains equivalent). If you had (a -> ((a' -> b') -> b')) and if you curried it with one element you would receive a function of type (a' -> b') -> b', yes.
2

In type signature, (->) is right associative, which implies that

a -> b -> c

which is the type of a function that takes an argument of type a and return another function of type b -> c, equals

a -> (b -> c)

However, it does not equals

(a -> b) -> c

which is the type of a function that takes another function of type a -> b as its only argument and return a value of type c.

Question 1:

How do i know which to take?

You should choose first version, as you already did, because

(a'->b'->b')->b'->[a']->b'

equals 

(a'->b'->b')->(b'->[a']->b')

And this is called currying, not greedy.

Question 2:

Why can i remove them when you cannot remove those in the original foldr

The same reason.

Improve this answer

Comments

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.