[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...

Jan Stolarek jan.stolarek at p.lodz.pl
Tue Jan 13 13:13:24 UTC 2015

> What does “~” mean…(it’s something that comes out in error messages when my
> types are all messed up)….
It means GHC knows that two types are equal.

> and then there’s a “=>” going on…in the middle of 
> a signature….I know “=>” in the context of “Num a => a -> a -> a”
Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of 
type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a 
practical example, though perhaps it's not the simplest one:


This code is thought as an intermediate level tutorial - you might want to give it a try. Another 
example I have is here (I use the name subst, but it's identical to gcastWith):




More information about the Haskell-Cafe mailing list