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