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@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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users