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?
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
participants (2)
-
Guy -
James Cook