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 <simo...@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-boun...@haskell.org> *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 > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
