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

[Oliver Charles]

On Tue, Jan 13, 2015 at 12:39 PM, Nicholls, Mark <nicholls.mark at vimn.com>
wrote:

>  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”
>

a ~ b is a constraint that a and b are exactly the same type. For example,
Int ~ Int is satisfiable, but Int ~ Bool is not. So what gcastWith does is
take a witness that a and b are the same type (witnessed by the a :~: b
value), and then lets you form a value using that evidence.


 What would a value of type “((a ~ b) => r)” look like?
>
>
I can't come up with a workable example right now, but I could imagine that
you might have:

   reverseReverse :: a :~: (Reverse (Reverse a))

Then if you have something that needs to work on a Reverse (Reverse a)
value, but you only have a 'a' around, you can show GHC that it doesn't
matter - because they are the same type:

  gcastWith reverseReverse :: (a ~ Reverse (Reverse a) => r) -> r

Presumably whatever 'r' is will refer to 'a' and do something with it
(maybe mapping over a list or something).

Sorry that this is all fairly vague, but hopefully that gives you some
leads.

-- ocharles
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150113/86178cf7/attachment.html>