[Haskell-beginners] ~ type operator

[James Cook]

On Jun 24, 2011, at 7:44 AM, Guy wrote:

> On 24/06/2011 12:10, Daniel Fischer wrote:
>> On Friday 24 June 2011, 10:26:42, Guy wrote:
>>> What does the ~ type operator mean? I've sometimes seen types such  
>>> as (a
>>> ~ b) in error messages, but can't understand what GHC is trying to  
>>> tell
>>> me.
>>
>> Type equality, (a ~ b) means that a and b are the same type  
>> (rather, that
>> the compiler can prove they're the same).
>
> So where is it useful to say a ~ b, rather than using a twice?

The original motivation, I believe, was for use with a some of the  
more advanced type system extensions: type families and GADTs   
(apologies if you haven't run across these before; I'm not going to  
give a detailed explanation of them because Google already has that  
covered, just a couple of examples assuming familiarity with them).

In code using the vector-space[1] package, you might wish to use a  
constraint such as:

 > Scalar a ~ Scalar b => ...

Scalar is essentially a type-level function, and this constraint  
asserts that it maps two different types to the same type.

In the process of type-checking code using GADTs, GHC will also  
"discover" type equalities that may not be obvious.  For example,

 > data Eq a b where Refl :: Eq a a
 >
 > coerce :: Eq a b -> a -> b
 > coerce Refl x = x

When checking this code, GHC infers that within the definition of  
'coerce', x has a type something like "a ~ b => a".  Which is to say,  
'a' and 'b' are still distinct type variables, but they happen to  
provably have the same value (in this particular context).

-- James

[1] http://hackage.haskell.org/package/vector-space