Natural number comparisons with evidence

[Conal Elliott]

I'm glad to know. Thanks for the endorsement, Richard.

On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

> Just to add my 2 cents: I've played in this playground and used the same
> structures as David. I second his suggestions.
>
> Richard
>
>
> On May 24, 2018, at 3:54 PM, Conal Elliott <conal at conal.net> wrote:
>
> Great! Thanks for the suggestion to use type equality and coerced `Refl`.
> - Conal
>
> On Thu, May 24, 2018 at 10:43 AM, David Feuer <david.feuer at gmail.com>
> wrote:
>
>> On Thu, May 24, 2018, 1:03 PM 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
>>>
>>
>> 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.
>>
>> -- Better, because there's only one Refl
>> unsafeEqual :: forall a b. a :~: b
>> unsafeEqual :: unsafeCoerce Refl
>>
>> unsafeWithEqual :: forall a b r. (a ~ b => r) -> r
>> unsafeWithEqual r
>>   | Refl <- unsafeEqual @a @b = r
>>
>> compareEv = case .... of
>>   LT -> unsafeWithEqual @(CmpNat u v) @LT CompareLT
>>   ...
>>
>>
>>> 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
>>>>>
>>>>
>>>
> _______________________________________________
> 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/c95a3842/attachment.html>