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

Tue Jan 13 17:29:50 UTC 2015

Brilliant!

Let my cogs turn....slowly...

I think the problem I will have writing these proofs, is how much the compiler "knows" at a given point is not especially clear....you have to build a mental model of what its doing.

Interesting stuff though.

From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
Sent: 13 January 2015 5:13 PM
To: Nicholls, Mark
Cc: haskell-cafe
Subject: Re: [Haskell-cafe] working my way through Data.Type.Equality...my head hurts...

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<mailto: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
CONFIDENTIALITY NOTICE

This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.

While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.

Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.

MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe.  MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150113/ac221b5b/attachment.html>