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

Nicholls, Mark nicholls.mark at vimn.com
Tue Jan 13 13:14:43 UTC 2015

It is fairly vague…I think it gets me to understand in a hand wavy sort of way.

Let me look a little deeper.

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

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


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/a7e69bb5/attachment.html>

More information about the Haskell-Cafe mailing list