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
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries