I'm glad to know. Thanks for the endorsement, Richard. On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg <r...@cs.brynmawr.edu> wrote:
> Just to add my 2 cents: I've played in this playground and used the same > structures as David. I second his suggestions. > > Richard > > > On May 24, 2018, at 3:54 PM, Conal Elliott <co...@conal.net> wrote: > > Great! Thanks for the suggestion to use type equality and coerced `Refl`. > - Conal > > On Thu, May 24, 2018 at 10:43 AM, David Feuer <david.fe...@gmail.com> > wrote: > >> 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 > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
