Natural number comparisons with evidence

[David Feuer]

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/20180523/ffb5c765/attachment.html>