On Thu, May 24, 2018, 1:03 PM Conal Elliott <co...@conal.net> wrote: > 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 >
This doesn't really smell right to me, no. Dict @() is actually a rather different value than you seek. In general, these look like they do way more than they ever can. I would suggest you look through those comparison *constraints* to the underlying type equalities involving the primitive CmpNat type family. -- Better, because there's only one Refl unsafeEqual :: forall a b. a :~: b unsafeEqual :: unsafeCoerce Refl unsafeWithEqual :: forall a b r. (a ~ b => r) -> r unsafeWithEqual r | Refl <- unsafeEqual @a @b = r compareEv = case .... of LT -> unsafeWithEqual @(CmpNat u v) @LT CompareLT ... > 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.fe...@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 <co...@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 >>> >> >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
