<div dir="ltr">Oh, yes---`sameNat` is indeed quite similar to my `compareEv`. I hadn't noticed. Thanks, Simon.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, May 24, 2018 at 2:30 PM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">





<div lang="EN-GB" link="#0563C1" vlink="#954F72">
<div class="m_-2232369221408389588WordSection1">
<p class="MsoNormal"><span>I see this in GHC.TypeNats<u></u><u></u></span></p>
<p class="m_-2232369221408389588Code"><b><span>sameNat ::</span></b><span>
<b>(KnownNat a, KnownNat b) =><u></u><u></u></b></span></p>
<p class="m_-2232369221408389588Code"><b><span>           Proxy a -> Proxy b -> Maybe (a :~: b)<u></u><u></u></span></b></p>
<p class="m_-2232369221408389588Code"><b><span>sameNat x y<u></u><u></u></span></b></p>
<p class="m_-2232369221408389588Code"><b><span>  | natVal x == natVal y = Just (unsafeCoerce Refl)<u></u><u></u></span></b></p>
<p class="m_-2232369221408389588Code"><b><span>  | otherwise            = Nothing<u></u><u></u></span></b></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>The unsafeCoerce says that sameNat is part of the trusted code base.  And indeed, it’s only because SNat is a private newtype (i.e its data constructor is private to GHC.TypeNats) that you can’t
 bogusly say    (SNat 7 :: SNat 8)<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>You want exactly the same thing, but for a comparison oriented data CompareEv, rather than its equality counterpart :~:.   So the same approach seems legitimate.
<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>I always want code with unsafeCoerce to be clear about (a) why it’s necessary and (b) why it’s sound.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Glasgow-haskell-users <<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-<wbr>bounces@haskell.org</a>>
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 24 May 2018 00:39<br>
<b>To:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.<wbr>org</a><br>
<b>Subject:</b> Natural number comparisons with evidence<u></u><u></u></span></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">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:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">> data CompareEv u v</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>   = (u < v) => CompareLT</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>   | (u ~ v) => CompareEQ</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>   | (u > v) => CompareGT</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Then I'd like to define a comparison operation (to be used with `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy arguments):<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">With `compareEv`, we can bring evidence into scope in `case` expressions.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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`):<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>               LT -> CompareLT</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>               EQ -> CompareEQ</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">>               GT -> CompareGT</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Can `compareEv` be implemented in GHC Haskell? Is there already an implementation of something similar? Any other advice?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Thanks,  -- Conal<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
</div></div></div>
</div>
</div>

</blockquote></div><br></div>