[Haskell-cafe] why different type variables enforce different types?
hyarion at iinet.net.au
Wed Aug 1 06:10:52 UTC 2018
On 01/08/18 15:49, Rui Azevedo wrote:
> after using haskell for a while i was surprised by this little thing
> 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?
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.
More information about the Haskell-Cafe