Polymorphism in Haskell

Question

I'm new to Haskell and reading Haskell from first principles.

BTW this question is general not related to this book, I have taken following question as example

In Chapter 10, Section 10.5, Q 5, part f

Question:

The following are simple folds very similar to what you’ve already seen, but each has at least one error. Please fix them and test in your REPL

f) foldr const 'a' [1..5]

and its giving this following Error No instance for (Num Char) arising from the literal `1'

simply means that 1 can not be used as Char here

but I read in this chapter that folds are Like Text Rewriter, replace cons(:) with the function and replace empty list with Accumulator so the result is (I have shorten the list)

foldr const 'a' [1..2] 
to 
(1 `const` (2 `const` 'a')) 

and its working no complier error

So what could went wrong ? why first one is not working and its rewritten is working ?

but I'm seeing in rewritten form const has two forms

Int -> Int -> Int 
and 
Int -> Char -> Int

maybe this is bcs of it so I Fix the type of const like this

cont :: Int -> Int -> Int
cont = const

and now When I stated using it

(1 `cont` (2 `cont` 'a'))

Couldn't match expected type `Int' with actual type `Char'

Seems like When We are using Polymorphic functions Haskell fix it type, and we can not use it in other form

maybe it should be list folds description should be like this

folds are Like Text Rewriter, replace cons(:) with the function, fix the type of function and replace empty list with Accumulator

Please share your thought about it.

not only Haskell but other typed languages has same behavior ?

or maybe I'm totally wrong ?

Answer 1

In the expression

(1 `const` (2 `const` 'a')) 
   ---A---    ---B---

we use the polymorphic function const twice. Each use causes the polymorphic function type to be instantiated to whatever type is needed to make everything type check.

The general type of const is:

const :: a -> b -> a

Let's assume that numeric literals have type Int to keep the explanation simple. When we write 2 `const` 'a' (point --B-- above), Haskell understands that type variable a above must be Int, while b must be Char, so here we are using

const :: Int -> Char -> Int

Therefore, the result of 2 `const` 'a' is of type Int.

Knowing that, we can now realize that the const used at point --A-- above can type check only if we choose both type variables a and b as Int. So, we are using

const :: Int -> Int -> Int

This is possible since the type system allows a distinct polymorphic type instantiation at each point the function is used.

---

It might be interesting to note that the expression

(\c -> 1 `c` (2 `c` 'a')) const

is an expression that simplifies (technically: beta-reduces) to the original one, but is not typeable. Here, const is used only once, so its type can be instantiated only once, but there is no single type instantiation that can be used in both c points. This is a known limitation of the type inference engine, shared among all the functional languages that perform Hindley-Milner inference.

Your use of foldr const .... shares the same issue.

It might be puzzling at first to see that we might have two expressions, one reducing to the other, but such that only one of them is typeable. However, this is a fact of life. Theoretically, Haskell satisfies the following "subject reduction" property:

• if expression e1 is typed, and e1 reduces to expression e2, then expression e2 is typed

However, Haskell (like most languages) fails to satisfy the following "subject expansion" property:

• if expression e2 is typed, and e1 reduces to expression e2, then expression e1 is typed

So, while it is impossible that a typed expression reduces to an ill-typed one, it is possible that an ill-typed expression reduces to a typed one. One example is the one you found. A simpler one is (\x -> True) ("ill-typed" "term") which is ill-typed (it uses a string as a function) but simplifies to True which is well-typed.

Answer 2

So what could went wrong ? why first one is not working and its rewritten is working ?

That's an interesting question which I feel is worth a little bit of explanation.

Firstly, the foldr example doesn't work because, as the compiler tells you, the types just don't match. foldr has the following type, when restricted to lists, which I'll write in a way that "matches up" with the arguments you're trying to give it

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

from which we see that the type variables a and b must take specific values - a must be a number (you can think of it as just Int, although it actually has the "polymorphic number" type, Num a => a, ie it can be any numeric type), while b must be char. So this only works if const can have a type like

Int -> Char -> Char

or the same with Int replaced by any numeric type.

But it doesn't matter what numeric type you choose, unless (as the compiler points out) you somehow define a Num instance for Char. That's because const has type

a -> b -> a

so to match with the above, a and b must both be Char, which means the numeric type (which I've assumed to be Int above, for simplicity) must be Char. Since that isn't one (but could in theory be made one, not that it would be a sensible idea), the compiler error message should I hope make sense now.

So why does the "longhand" form that you quote:

(1 `const` (2 `const` 'a')) 

work? This is certainly what the above foldr would be equivalent too, if it compiled. But it doesn't logically follow from this that, when the foldr fails to compile, so must the above. It works because const is a polymorphic function - it can apply to literally any 2 arguments, of any type, and returns the first one. So it reduces successively to (again I've simplified by using simply Int for any numeric type):

1 `const` 2

(using const :: Int -> Char -> Int)

1

(using const :: Int -> Int -> Int)

Note that the 2 invocations of const actually have 2 different types. This is fine, since const is polymorphic. But it's not fine to pass const into foldr and expect it to have different types each time it is invoked inside foldr.

That's not any kind of general rule, at least if you use the RankNTypes language extension. Using that extension you can define functions that accept a polymorphic function as argument and then apply it with different types:

example :: (forall a. a -> a) -> (Int, Bool)
example f = (f 1, f True)

But the signature of foldr (shown above) is nothing like this. Although the a and b in its type signature are free to vary, the a is forced to be a numeric type because you pass it a numeric list, while the b is forced to be Char due to the accumulator of 'a'- so the only "version" of const that could ever work is the one of type (again, specialising the numeric type for simplicity) Int -> Char -> Char, which isn't a possible type for const.

Answer 3

Your analysis is correct, though it's a bit down in the details. You can see the problem at a bit higher level, if you like.

foldr :: (a -> r -> r) -> r -> [a] -> r
const :: b -> c -> b

(Forgive me if I've picked different type variables than you're used to - alpha equivalence says the variable names don't matter and keeping names different makes it easier to see what's going on.)

If you use those types and unify things to make foldr const work, you get something like this:

(a -> r -> r) ~ (b -> c -> b)
a ~ b (first arg)
r ~ c (second arg)
r ~ b (result)
r ~ a (by transitivity)

foldr const :: a -> [a] -> a (substitution)

Where ~ means "these types are the same".

So you can see just from foldr and const the the type of the elements of the list must unify with the type of the other argument.

You are correct, though, that if the foldr there was inlined in its entirety before type checking, the resulting expression would check successfully. But that's a bit of an insufficient situation. What if you did foldr const 'a' []? Since that would reduce to 'a', it would also type check - but it would do so with a different type than if the list passed to it was non-empty.

And that's exactly the kind of problem the Haskell type system is intended to prevent. An expression's type should be derived entirely from the types of its subexpressions. Values should never(*) be considered, so an expression needs to have the same result type regardless if whether a subexpression is an empty list or non-empty.

(*) Ok, GHC supports a bit more than Haskell 2010. Extensions like GADTs can enable a form of types depending on values, but only in very specific ways that maintain larger coherent properties.

Answer 4

I think, it's simpler, and the function const just doesn't fit the signature expected by the foldr:

Prelude> :t foldr
foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
Prelude> :t const
const :: a -> b -> a

So haskell tries to generalize both of a and b (to find out, both of them have sufficient set of typeclasses), and, finally, figures out that 1 is a number, but 'c' doesn't implement this typeclass.