[Haskell-beginners] ~ type operator
mokus at deepbondi.net
Fri Jun 24 16:34:37 CEST 2011
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
>> 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 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).
More information about the Beginners