Natural number comparisons with evidence
rae at cs.brynmawr.edu
Thu May 24 20:05:32 UTC 2018
Just to add my 2 cents: I've played in this playground and used the same structures as David. I second his suggestions.
> On May 24, 2018, at 3:54 PM, Conal Elliott <conal at 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.feuer at gmail.com <mailto:david.feuer at gmail.com>> wrote:
> On Thu, May 24, 2018, 1:03 PM Conal Elliott <conal at conal.net <mailto:conal at 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.feuer at gmail.com <mailto:david.feuer at 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 <conal at conal.net <mailto:conal at 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 at haskell.org <mailto:Glasgow-haskell-users at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users <http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users>
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users