[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...
eir at cis.upenn.edu
Tue Jan 13 17:12:39 UTC 2015
Permit me to take a stab from the beginning.
On Jan 13, 2015, at 7:39 AM, "Nicholls, Mark" <nicholls.mark at vimn.com> wrote:
> Full code here…
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)
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
> Ø -- | 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!
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe