[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...
Oliver Charles
ollie at ocharles.org.uk
Tue Jan 13 12:51:30 UTC 2015
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>
More information about the Haskell-Cafe
mailing list