Re: Natural number comparisons with evidence

Oh, yes---`sameNat` is indeed quite similar to my `compareEv`. I hadn't noticed. Thanks, Simon. On Thu, May 24, 2018 at 2:30 PM, Simon Peyton Jones wrote:

I see this in GHC.TypeNats

*sameNat ::* *(KnownNat a, KnownNat b) =>*

* Proxy a -> Proxy b -> Maybe (a :~: b)*

*sameNat x y*

* | natVal x == natVal y = Just (unsafeCoerce Refl)*

* | otherwise = Nothing*

The unsafeCoerce says that sameNat is part of the trusted code base. And indeed, it’s only because SNat is a private newtype (i.e its data constructor is private to GHC.TypeNats) that you can’t bogusly say (SNat 7 :: SNat 8)

You want exactly the same thing, but for a comparison oriented data CompareEv, rather than its equality counterpart :~:. So the same approach seems legitimate.

I always want code with unsafeCoerce to be clear about (a) why it’s necessary and (b) why it’s sound.

Simon

*From:* Glasgow-haskell-users *On Behalf Of *Conal Elliott *Sent:* 24 May 2018 00:39 *To:* glasgow-haskell-users@haskell.org *Subject:* Natural number comparisons with evidence

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