Hi Mark,
Permit me to take a stab from the beginning.
On Jan 13, 2015, at 7:39 AM, "Nicholls, Mark"
Full code here… https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs
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...)
I hope this helps! Richard