Natural number comparisons with evidence

[Conal Elliott]

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/915423ae/attachment.html>