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