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
