[Haskell-cafe] why different type variables enforce different types?

[Ben]

On 01/08/18 15:49, Rui Azevedo wrote:
> after using haskell for a while i was surprised by this little thing
>
> f::a->b
> f a=a
>
> and this is not making sense to me till now, so please can someone 
> enlighten me, why does haskell assume that b can not be the same type 
> of a?
>
> after all having two distinct math variables does not mean they can 
> not have the same value.
>
> I know i could use f::a->a, but its not the same thing, on this last 
> case I'm requesting them to be the same type, but on the first I'm not 
> forbidding it, is there a math reason behind it?
>
> would type inference be rendered impossible if considering the case of 
> them being equal?
>
> thanks

Hi Rui,

Haskell does not assume that a and b cannot be the same type. If you had 
some `f :: a -> b`, then it would happily let you use f at the type `f 
:: Int -> Int`, no problem.

What it does is make sure that *you* do not write code that *does* 
assume they are the same type. Your implementation `f a = a` can *only* 
work when a and b are the same type. The type signature `f :: a -> b` 
allows them to be the same, but also allows them to be different, so the 
code implementing that type signature must be able to work regardless of 
whether to not they are the same.

If you write just the code `f a = a` and leave off the type signature, 
GHC will infer the type `f :: a -> a` just fine. Type inference is 
perfectly possible while considering the case of them being equal (in 
fact it figures out that they *must* be equal). But if you write both 
the type `f :: a -> b` and the code `f a = a`, then GHC considers them 
both as fixed constraints that you have written, so it gives you an 
error when it proves that they cannot fit together.

Hopefully that makes more sense to you.

Regards,
Ben