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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
where `Dict` is from Ed Kmett's constraints library (https://hackage.haskell.org/package/constraints). On Thu, May 24, 2018 at 10:03 AM, Conal Elliott <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Conal Elliott
On Thu, May 24, 2018, 1:03 PM Conal Elliott <[hidden email]> wrote:
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 ...
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Great! Thanks for the suggestion to use type equality and coerced `Refl`. - Conal On Thu, May 24, 2018 at 10:43 AM, David Feuer <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Just to add my 2 cents: I've played in this playground and used the same structures as David. I second his suggestions.
Richard
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
I'm glad to know. Thanks for the endorsement, Richard. On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Conal Elliott
I see this in GHC.TypeNats sameNat ::
(KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) sameNat x y | natVal x == natVal y = Just (unsafeCoerce Refl) | otherwise = Nothing The unsafeCoerce says that sameNat is part of the trusted code base. And indeed, it’s only because SNat is a private newtype (i.e its data constructor is private to GHC.TypeNats) that you can’t
bogusly say (SNat 7 :: SNat 8) You want exactly the same thing, but for a comparison oriented data CompareEv, rather than its equality counterpart :~:. So the same approach seems legitimate.
I always want code with unsafeCoerce to be clear about (a) why it’s necessary and (b) why it’s sound. Simon From: Glasgow-haskell-users <[hidden email]>
On Behalf Of Conal Elliott 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
Oh, yes---`sameNat` is indeed quite similar to my `compareEv`. I hadn't noticed. Thanks, Simon. On Thu, May 24, 2018 at 2:30 PM, Simon Peyton Jones <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Conal Elliott
To throw out additional related work, I had a need for runtime values that capture type-level naturals. It’s used primarily for representing the widths in a type-safe bitvector formulas.
The code is a few years old, but publicly available here: https://github.com/GaloisInc/parameterized-utils/blob/master/src/Data/Parameterized/NatRepr.hs I’d be interested in knowing if there are now any comprehensive libraries for doing this sort of runtime reflection of type-level naturals. Regards, Joe > On May 24, 2018, at 1:07 PM, Conal Elliott <[hidden email]> wrote: > > I'm glad to know. Thanks for the endorsement, Richard. > > On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> wrote: >> On Thu, May 24, 2018, 1:03 PM Conal Elliott <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >> >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > > > _______________________________________________ > Glasgow-haskell-users mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users signature.asc (849 bytes) Download Attachment |
Free forum by Nabble | Edit this page |