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.