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 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
