<div dir="ltr">This seems like the kind of thing that first should be fleshed out in its own package. Is there some reason that this module would need to be in base?<br><br><div class="gmail_quote"><div dir="ltr">On Thu, Jul 6, 2017 at 1:56 PM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That seems generally reasonable to me. It'll need the usual discussion<br>
process here and then it can be added to `base`. However, I think it<br>
should not be added to `Data.Type.Equality`, but rather to a new<br>
module, perhaps `Data.Type.Equality.Heterogeneous`. That module will<br>
then be able to offer the full complement of basic functions (sym,<br>
trans, ...) without stepping on the pre-existing names. I imagine<br>
you'll also want one or two extra casting operations, and conversions<br>
between `:~:` and `:~~:`. Also, you have called the constructor of<br>
this type HRefl in the past, which strikes me as better than Refl.<br>
<br>
David<br>
<br>
On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch<br>
<<a href="mailto:wolfgang-it@jeltsch.info" target="_blank">wolfgang-it@jeltsch.info</a>> wrote:<br>
> Hi!<br>
><br>
> The module Data.Type.Equality in the base package contains the type<br>
> (:~:) for homogeneous equality. However, a type for heterogeneous<br>
> equality would be very useful as well. I would define such a type as<br>
> follows:<br>
><br>
>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}<br>
>><br>
>> data (a :: k) :~~: (b :: l) where<br>
>><br>
>>     Refl :: a :~~: a<br>
><br>
> Is there already such a type in the base package? If not, does it make<br>
> sense to file a feature request (or would such a proposal be likely to<br>
> not being accepted for some reason)?<br>
><br>
> All the best,<br>
> Wolfgang<br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div>