Natural number comparisons with evidence

[Conal Elliott]

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