Natural number comparisons with evidence

[Conal Elliott]

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 <simonpj at microsoft.com>
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 <glasgow-haskell-users-bounces at haskell.org> *On
> Behalf Of *Conal Elliott
> *Sent:* 24 May 2018 00:39
> *To:* glasgow-haskell-users at 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20180524/b660c195/attachment.html>