<div dir="ltr">where `Dict` is from Ed Kmett's constraints library (<a href="https://hackage.haskell.org/package/constraints">https://hackage.haskell.org/package/constraints</a>).</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, May 24, 2018 at 10:03 AM, Conal Elliott <span dir="ltr"><<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Thanks for this suggestion, David. It seems to work out well, though I haven't tried running yet.</div><div><br></div><div><font face="monospace, monospace">> unsafeDict :: Dict c</font></div><div><font face="monospace, monospace">> unsafeDict = unsafeCoerce (Dict @ ())</font></div><div><font face="monospace, monospace">></font></div><div><font face="monospace, monospace">> unsafeSatisfy :: forall c a. (c => a) -> a</font></div><div><font face="monospace, monospace">> unsafeSatisfy z | Dict <- unsafeDict @ c = z</font></div><div><br></div><div>Now we can define `compareEv`:</div><div><br></div><div><font face="monospace, monospace">> compareEv :: forall u v. KnownNat2 u v => CompareEv u v</font></div><div><font face="monospace, monospace">> compareEv = case natValAt @ u `compare` natValAt @ v of</font></div><div><font face="monospace, monospace">>               LT -> unsafeSatisfy @ (u < v) CompareLT</font></div><div><font face="monospace, monospace">>               EQ -> unsafeSatisfy @ (u ~ v) CompareEQ</font></div><div><font face="monospace, monospace">>               GT -> unsafeSatisfy @ (u > v) CompareGT</font></div><div><br></div><div>If anyone has other techniques to suggest, I'd love to hear.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>-- Conal</div><div><br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 23, 2018 at 5:44 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">I think the usual approach for defining these sorts of primitive operations is to use unsafeCoerce.</div><br><div class="gmail_quote"><div><div class="m_6356850797392718668h5"><div dir="ltr">On Wed, May 23, 2018, 7:39 PM Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:<br></div></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_6356850797392718668h5"><div dir="ltr"><div>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><br></div><div><font face="monospace, monospace">> data CompareEv u v</font></div><div><font face="monospace, monospace">>   = (u < v) => CompareLT</font></div><div><font face="monospace, monospace">>   | (u ~ v) => CompareEQ</font></div><div><font face="monospace, monospace">>   | (u > v) => CompareGT</font></div><div><br></div><div>Then I'd like to define a comparison operation (to be used with `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy arguments):</div><div><br></div><div><font face="monospace, monospace">> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v</font></div><div><br></div><div>With `compareEv`, we can bring evidence into scope in `case` expressions.</div><div><br></div><div>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><br></div><div><font face="monospace, monospace">> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of</font></div><div><font face="monospace, monospace">>               LT -> CompareLT</font></div><div><font face="monospace, monospace">>               EQ -> CompareEQ</font></div><div><font face="monospace, monospace">>               GT -> CompareGT</font></div><div><br></div><div>Can `compareEv` be implemented in GHC Haskell? Is there already an implementation of something similar? Any other advice?</div><div><br></div><div>Thanks,  -- Conal</div><div><br></div></div></div></div>
______________________________<wbr>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" rel="noreferrer" target="_blank">Glasgow-haskell-users@haskell.<wbr>org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/glasgow-has<wbr>kell-users</a><br>
</blockquote></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>