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

[Richard Eisenberg]

Hi Mark,

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…
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150113/4257d339/attachment.html>