<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Just to add my 2 cents: I've played in this playground and used the same structures as David. I second his suggestions.<div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On May 24, 2018, at 3:54 PM, Conal Elliott <<a href="mailto:conal@conal.net" class="">conal@conal.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Great! Thanks for the suggestion to use type equality and coerced `Refl`. - Conal<br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Thu, May 24, 2018 at 10:43 AM, David Feuer <span dir="ltr" class=""><<a href="mailto:david.feuer@gmail.com" target="_blank" class="">david.feuer@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto" class=""><span class=""><div class=""><div class="gmail_quote"><div dir="ltr" class="">On Thu, May 24, 2018, 1:03 PM Conal Elliott <<a href="mailto:conal@conal.net" target="_blank" class="">conal@conal.net</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class=""><div class="">Thanks for this suggestion, David. It seems to work out well, though I haven't tried running yet.</div><div class=""><br class=""></div><div class=""><font face="monospace, monospace" class="">> unsafeDict :: Dict c</font></div><div class=""><font face="monospace, monospace" class="">> unsafeDict = unsafeCoerce (Dict @ ())</font></div><div class=""><font face="monospace, monospace" class="">></font></div><div class=""><font face="monospace, monospace" class="">> unsafeSatisfy :: forall c a. (c => a) -> a</font></div><div class=""><font face="monospace, monospace" class="">> unsafeSatisfy z | Dict <- unsafeDict @ c = z</font></div></div></blockquote></div></div><div dir="auto" class=""><br class=""></div></span><div dir="auto" class="">This doesn't really smell right to me, no. Dict @() is actually a rather different value than you seek. In general, these look like they do way more than they ever can. I would suggest you look through those comparison *constraints* to the underlying type equalities involving the primitive CmpNat type family.</div><div dir="auto" class=""><br class=""></div><div dir="auto" class="">-- Better, because there's only one Refl</div><div dir="auto" class="">unsafeEqual :: forall a b. a :~: b</div><div dir="auto" class="">unsafeEqual :: unsafeCoerce Refl</div><div dir="auto" class=""><br class=""></div><div dir="auto" class="">unsafeWithEqual :: forall a b r. (a ~ b => r) -> r</div><div dir="auto" class="">unsafeWithEqual r</div><div dir="auto" class=""> | Refl <- unsafeEqual @a @b = r</div><div dir="auto" class=""><br class=""></div><div dir="auto" class="">compareEv = case .... of</div><div dir="auto" class=""> LT -> unsafeWithEqual @(CmpNat u v) @LT CompareLT</div><div dir="auto" class=""> ...</div><div class=""><div class="h5"><div dir="auto" class=""><br class=""></div><div dir="auto" class=""><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Now we can define `compareEv`:</div><div class=""><br class=""></div><div class=""><font face="monospace, monospace" class="">> compareEv :: forall u v. KnownNat2 u v => CompareEv u v</font></div><div class=""><font face="monospace, monospace" class="">> compareEv = case natValAt @ u `compare` natValAt @ v of</font></div><div class=""><font face="monospace, monospace" class="">> LT -> unsafeSatisfy @ (u < v) CompareLT</font></div><div class=""><font face="monospace, monospace" class="">> EQ -> unsafeSatisfy @ (u ~ v) CompareEQ</font></div><div class=""><font face="monospace, monospace" class="">> GT -> unsafeSatisfy @ (u > v) CompareGT</font></div><div class=""><br class=""></div><div class="">If anyone has other techniques to suggest, I'd love to hear.</div><div class=""><br class=""></div><div class="">-- Conal</div><div class=""><br class=""></div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Wed, May 23, 2018 at 5:44 PM, David Feuer <span dir="ltr" class=""><<a href="mailto:david.feuer@gmail.com" rel="noreferrer" target="_blank" class="">david.feuer@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto" class="">I think the usual approach for defining these sorts of primitive operations is to use unsafeCoerce.</div><br class=""><div class="gmail_quote"><div class=""><div class="m_-3398887638732496914m_-2101457337368815716h5"><div dir="ltr" class="">On Wed, May 23, 2018, 7:39 PM Conal Elliott <<a href="mailto:conal@conal.net" rel="noreferrer" target="_blank" class="">conal@conal.net</a>> wrote:<br class=""></div></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class=""><div class="m_-3398887638732496914m_-2101457337368815716h5"><div dir="ltr" class=""><div class="">When programming with GHC's type-level natural numbers and `KnownNat` constraints, how can one construct *evidence* of the result of comparisons to be used in further computations? For instance, we might define a type for augmenting the results of `compare` with evidence:</div><div class=""><br class=""></div><div class=""><font face="monospace, monospace" class="">> data CompareEv u v</font></div><div class=""><font face="monospace, monospace" class="">> = (u < v) => CompareLT</font></div><div class=""><font face="monospace, monospace" class="">> | (u ~ v) => CompareEQ</font></div><div class=""><font face="monospace, monospace" class="">> | (u > v) => CompareGT</font></div><div class=""><br class=""></div><div class="">Then I'd like to define a comparison operation (to be used with `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy arguments):</div><div class=""><br class=""></div><div class=""><font face="monospace, monospace" class="">> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v</font></div><div class=""><br class=""></div><div class="">With `compareEv`, we can bring evidence into scope in `case` expressions.</div><div class=""><br class=""></div><div class="">I don't know how to implement `compareEv`. The following attempt fails to type-check, since `compare` doesn't produce evidence (which is the motivation for `compareEv` over `compare`):</div><div class=""><br class=""></div><div class=""><font face="monospace, monospace" class="">> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of</font></div><div class=""><font face="monospace, monospace" class="">> LT -> CompareLT</font></div><div class=""><font face="monospace, monospace" class="">> EQ -> CompareEQ</font></div><div class=""><font face="monospace, monospace" class="">> GT -> CompareGT</font></div><div class=""><br class=""></div><div class="">Can `compareEv` be implemented in GHC Haskell? Is there already an implementation of something similar? Any other advice?</div><div class=""><br class=""></div><div class="">Thanks, -- Conal</div><div class=""><br class=""></div></div></div></div>
______________________________<wbr class="">_________________<br class="">
Glasgow-haskell-users mailing list<br class="">
<a href="mailto:Glasgow-haskell-users@haskell.org" rel="noreferrer noreferrer" target="_blank" class="">Glasgow-haskell-users@haskell.<wbr class="">org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer noreferrer noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-<wbr class="">bin/mailman/listinfo/glasgow-<wbr class="">haskell-users</a><br class="">
</blockquote></div>
</blockquote></div><br class=""></div>
</blockquote></div></div></div></div></div>
</blockquote></div><br class=""></div>
_______________________________________________<br class="">Glasgow-haskell-users mailing list<br class=""><a href="mailto:Glasgow-haskell-users@haskell.org" class="">Glasgow-haskell-users@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users<br class=""></div></blockquote></div><br class=""></div></body></html>