<div dir="auto">By the way.... the nicest version of the ad hoc equality would probably use a kind class:<div dir="auto"><br></div><div dir="auto">class TEq (k :: Type) where</div><div dir="auto"> type (==) (a :: k) (b :: k) :: Bool</div><div dir="auto"> type a == b = DefaultEq a b</div><div dir="auto"><br></div><div dir="auto">So then you could write</div><div dir="auto"><br></div><div dir="auto">instance TEq (Maybe k)</div><div dir="auto">instance TEq (Either j k)</div><div dir="auto">instance TEq [k]</div><div dir="auto">instance TEq (j -> k)</div><div dir="auto">instance TEq () where</div><div dir="auto"> type _ == _ = 'True</div><div dir="auto"><br></div><div dir="auto">etc.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Aug 10, 2017 1:46 AM, "David Feuer" <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">(==), in that option, is an open type family, and Equal (more likely a synonym dealing with its kind) is a helper function. Note that Equality, in this version, calls == to deal with arguments.<div dir="auto"><br></div><div dir="auto">type DefaultEq (a :: k) (b :: k) = Equal k a b</div><div dir="auto"><br></div><div dir="auto">Then if con1 and con2 are constructors,</div><div dir="auto"><br></div><div dir="auto">DefaultEq (con1 a b) (con2 c d) =</div><div dir="auto"> (con1 exactly equals con2) && a == c && b == d</div><div dir="auto"><br></div><div dir="auto">The == for the kinds of a/c and b/d could be anything a user wishes.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Aug 10, 2017 1:35 AM, "Ivan Lazar Miljenovic" <<a href="mailto:ivan.miljenovic@gmail.com" target="_blank">ivan.miljenovic@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 10 August 2017 at 14:44, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br>
> To be more specific about the ad hoc equality option, I'm thinking about<br>
> something like this (if it doesn't compile, I'm sure something similar<br>
> will):<br>
><br>
> type family (a :: k) == (b :: k) :: Bool<br>
> infix 4 ==<br>
><br>
> type family Equal (k :: Type) (a :: k) (b :: k) where<br>
> Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =<br>
> Equal (j -> k) f g && (a == b)<br>
> Equal k a a = 'True<br>
> Equal k a b = 'False<br>
><br>
> type instance (a :: Type) == b = Equal Type a b<br>
> type instance (a :: Maybe k) == b = Equal Type a b<br>
<br>
Since this is a closed type family, isn't doing any extra explicit<br>
type instances illegal?<br>
<br>
> ....<br>
><br>
> So for example, we'd get<br>
><br>
> 'Just (x :: k) == 'Just y<br>
> =<br>
> Equal (k -> Maybe k) 'Just && x == y<br>
> =<br>
> x == y<br>
><br>
> On Aug 10, 2017 12:29 AM, "David Feuer" <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br>
><br>
> The (==) type family in Data.Type.Equality was designed largely to calculate<br>
> structural equality of types. However, limitations of GHC's type system at<br>
> the type prevented this from being fully realized. Today, with TypeInType,<br>
> we can actually do it, replacing the boatload of ad hoc instances like so:<br>
><br>
> type (a :: k) == (b :: k) = Equal k a b<br>
> infix 4 ==<br>
><br>
> type family Equal (k :: Type) (a :: k) (b :: k) where<br>
> Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =<br>
> Equal (j -> k) f g && Equal j a b<br>
> Equal k a a = 'True<br>
> Equal k a b = 'False<br>
><br>
> This == behaves in a much more uniform way than the current one. I see two<br>
> potential causes for complaint:<br>
><br>
> 1. For types of kind *, the new version will sometimes fail to reduce when<br>
> the old one succeeded (and vice versa). For example, GHC currently accepts<br>
><br>
> eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True<br>
> eqeq _ = Refl<br>
><br>
> while the proposed version does not.<br>
><br>
> 2. Some users may want non-structural equality on their types for some<br>
> reason. The only example in base is<br>
><br>
> type instance (a :: ()) == (b :: ()) = 'True<br>
><br>
> which consists two types of kind () the same even if they're stuck types.<br>
> But perhaps someone wants to implement a non-trivial type-level data<br>
> structure with a special notion of equality.<br>
><br>
><br>
> I don't think (1) is really worth worrying too much about. For (2), if users<br>
> want to have control, we could at least use a mechanism similar to the above<br>
> to make the obvious instances easier to write.<br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<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-bi<wbr>n/mailman/listinfo/libraries</a><br>
><br>
<br>
<br>
<br>
--<br>
Ivan Lazar Miljenovic<br>
<a href="mailto:Ivan.Miljenovic@gmail.com" target="_blank">Ivan.Miljenovic@gmail.com</a><br>
<a href="http://IvanMiljenovic.wordpress.com" rel="noreferrer" target="_blank">http://IvanMiljenovic.wordpres<wbr>s.com</a><br>
</blockquote></div></div>
</blockquote></div></div>