Permit me to take a stab from the beginning.
First off, I should point out that Data.Type.Equality, while indeed served at the address above, is now a standard library. The code in that repo is identical to the version that ships with GHC 7.8.
Lets start at the beginning…
Ø data a :~: b where
Ø Refl :: a :~: a
Looks reasonable….” a :~: b” is inhabited by 1 value…of type “a :~: a”
This is true, but there's a bit more going on. If, say, we learn that the type `foo :~: bar` is indeed inhabited by `Refl`, then we know that `foo` and `bar` are the same types. That is
> baz :: foo :~: bar -> ...
> baz evidence = case evidence of
> Refl -> -- here, we may assume that `foo` and `bar` are fully identical
Conversely, whenever we *use* `Refl` in an expression, we must know that the two types being related are indeed equal.
Ø sym :: (a :~: b) -> (b :~: a)
Ø sym Refl = Refl
hmmm… (a :~: b) implies that a is b
so (b :~: a)
brilliant
Yes. After pattern-matching on `Refl`, GHC learns that `a` is identical to `b`. Thus, when we use `Refl` on the right-hand side, we know `b` is the same as `a`, and thus the use of `Refl` type checks.
Ø -- | Transitivity of equality
Ø trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
Ø trans Refl Refl = Refl
Ø -- | Type-safe cast, using propositional equality
Ø castWith :: (a :~: b) -> a -> b
Ø castWith Refl x = x
fine….
But….
Ø -- | Generalized form of type-safe cast using propositional equality
Ø gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
Ø gcastWith Refl x = x
I don’t even understand the signature
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”
While the comments I've seen about `~` are quite true, I think there's a simpler way to explain it. `~` is simply equality on types. The constraint `a ~ b` means that `a` is the same type as `b`. We could have spelled it `=` if that weren't used elsewhere. Before `~` was added to GHC, it might have been implemented like this:
> class Equals a b | a -> b, b -> a
> instance Equals x x
> -- no other instances!
The proper `~` works better in type inference than this functional-dependency approach, but perhaps rewriting `~` in terms of functional dependencies is illuminating.
When a constraint `a ~ b` is in the context, then GHC assumes the types are the same, and freely rewrites one to the other.
The type `(a ~ b) => r` above is a higher-rank type, which is why it may look strange to you. Let's skip the precise definition of "higher-rank" for now. In practical terms: let's say you write `gcastWith proof x` in your program. By the type signature of `gcastWith`, GHC knows that `proof` must have type `a :~: b` for some `a` and `b`. It further knows that `x` has the type `(a ~ b) => r`, for some `r`, but the same `a` and `b`. Of course, if a Haskell expression as a type `constraint => stuff`, then GHC can assume `constraint` when type-checking the expression. The same holds here: GHC assumes `a ~ b` (that is, `a` and `b` are identical) when type-checking the expression `x`. Perhaps, somewhere deep inside `x`, you pass a variable of type `a` to a function expecting a `b` -- that's just fine, because `a` and `b` are the same.
The `r` type variable in the type of `gcastWith` is the type of the result. It's the type you would naively give to `x`, but without a particular assumption that `a` and `b` are the same.
What would a value of type “((a ~ b) => r)” look like?
It looks just like a value of type `r`. Except that GHC has an extra assumption during type-checking. Contrast this to, say,
> min :: Ord a => a -> a -> a
> min = \x y -> if x < y then x else y
What does a value of `Ord a => a -> a -> a` look like? Identically to a value of type `a -> a -> a`, except with an extra assumption. This is just like the type `(a ~ b) => r`, just less exotic-looking.
As for singleton types and dependent types: they're great fun, but I don't think you need to go anywhere near there to understand this module. (Other modules in that repo, on the other hand, get scarier...)