On Tue, Jan 13, 2015 at 12:39 PM, Nicholls, Mark <nicholls.mark@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