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