Heterogeneous equality into base?

[Eric Mertens]

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?

On Thu, Jul 6, 2017 at 1:56 PM David Feuer <david.feuer at gmail.com> wrote:

> That seems generally reasonable to me. It'll need the usual discussion
> process here and then it can be added to `base`. However, I think it
> should not be added to `Data.Type.Equality`, but rather to a new
> module, perhaps `Data.Type.Equality.Heterogeneous`. That module will
> then be able to offer the full complement of basic functions (sym,
> trans, ...) without stepping on the pre-existing names. I imagine
> you'll also want one or two extra casting operations, and conversions
> between `:~:` and `:~~:`. Also, you have called the constructor of
> this type HRefl in the past, which strikes me as better than Refl.
>
> David
>
> On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
> <wolfgang-it at jeltsch.info> wrote:
> > Hi!
> >
> > The module Data.Type.Equality in the base package contains the type
> > (:~:) for homogeneous equality. However, a type for heterogeneous
> > equality would be very useful as well. I would define such a type as
> > follows:
> >
> >> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> >>
> >> data (a :: k) :~~: (b :: l) where
> >>
> >>     Refl :: a :~~: a
> >
> > Is there already such a type in the base package? If not, does it make
> > sense to file a feature request (or would such a proposal be likely to
> > not being accepted for some reason)?
> >
> > All the best,
> > Wolfgang
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170706/70ee04b5/attachment.html>