Natural number comparisons with evidence

[Conal Elliott]

where `Dict` is from Ed Kmett's constraints library (
https://hackage.haskell.org/package/constraints).

On Thu, May 24, 2018 at 10:03 AM, Conal Elliott <conal at conal.net> wrote:

> Thanks for this suggestion, David. It seems to work out well, though I
> haven't tried running yet.
>
> > unsafeDict :: Dict c
> > unsafeDict = unsafeCoerce (Dict @ ())
> >
> > unsafeSatisfy :: forall c a. (c => a) -> a
> > unsafeSatisfy z | Dict <- unsafeDict @ c = z
>
> Now we can define `compareEv`:
>
> > compareEv :: forall u v. KnownNat2 u v => CompareEv u v
> > compareEv = case natValAt @ u `compare` natValAt @ v of
> >               LT -> unsafeSatisfy @ (u < v) CompareLT
> >               EQ -> unsafeSatisfy @ (u ~ v) CompareEQ
> >               GT -> unsafeSatisfy @ (u > v) CompareGT
>
> If anyone has other techniques to suggest, I'd love to hear.
>
> -- Conal
>
>
> On Wed, May 23, 2018 at 5:44 PM, David Feuer <david.feuer at gmail.com>
> wrote:
>
>> I think the usual approach for defining these sorts of primitive
>> operations is to use unsafeCoerce.
>>
>> On Wed, May 23, 2018, 7:39 PM Conal Elliott <conal at conal.net> wrote:
>>
>>> 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:
>>>
>>> > data CompareEv u v
>>> >   = (u < v) => CompareLT
>>> >   | (u ~ v) => CompareEQ
>>> >   | (u > v) => CompareGT
>>>
>>> Then I'd like to define a comparison operation (to be used with
>>> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
>>> arguments):
>>>
>>> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>>>
>>> With `compareEv`, we can bring evidence into scope in `case` expressions.
>>>
>>> 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`):
>>>
>>> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>>> >               LT -> CompareLT
>>> >               EQ -> CompareEQ
>>> >               GT -> CompareGT
>>>
>>> Can `compareEv` be implemented in GHC Haskell? Is there already an
>>> implementation of something similar? Any other advice?
>>>
>>> Thanks,  -- Conal
>>>
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20180524/e44c4704/attachment.html>