Natural number comparisons with evidence

Conal Elliott conal at conal.net
Thu May 24 19:54:58 UTC 2018


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
>>>>
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20180524/221c6733/attachment.html>


More information about the Glasgow-haskell-users mailing list