Natural number comparisons with evidence

newer
The dreaded windows path length...

Conal Elliott

23 May 2018 23 May '18

7:38 p.m.

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

Attachments:

attachment.html (text/html — 1.9 KB)

Show replies by date

David Feuer

23 May 23 May

8:44 p.m.

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

Conal Elliott

24 May 24 May

1:03 p.m.

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

Conal Elliott

1:10 p.m.

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

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

David Feuer

1:43 p.m.

On Thu, May 24, 2018, 1:03 PM Conal Elliott 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 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 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

Conal Elliott

3:54 p.m.

Great! Thanks for the suggestion to use type equality and coerced `Refl`. - Conal On Thu, May 24, 2018 at 10:43 AM, David Feuer wrote:

...

On Thu, May 24, 2018, 1:03 PM Conal Elliott 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 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 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

Richard Eisenberg

4:05 p.m.

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 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 mailto:david.feuer@gmail.com> wrote: On Thu, May 24, 2018, 1:03 PM Conal Elliott mailto:conal@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 mailto:david.feuer@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 mailto:conal@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 mailto:Glasgow-haskell-users@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Conal Elliott

4:07 p.m.

I'm glad to know. Thanks for the endorsement, Richard. On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg 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 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 wrote:

...
On Thu, May 24, 2018, 1:03 PM Conal Elliott 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 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 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

Joe Hendrix

7:26 p.m.

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/Parame... 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 wrote:

I'm glad to know. Thanks for the endorsement, Richard.

On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg 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 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 wrote: On Thu, May 24, 2018, 1:03 PM Conal Elliott 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 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 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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Simon Peyton Jones

5:30 p.m.

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 On Behalf Of Conal Elliott Sent: 24 May 2018 00:39 To: glasgow-haskell-users@haskell.org Subject: Natural number comparisons with evidence 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

...

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

Conal Elliott

6:53 p.m.

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

...

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 *On Behalf Of *Conal Elliott *Sent:* 24 May 2018 00:39 *To:* glasgow-haskell-users@haskell.org *Subject:* Natural number comparisons with evidence

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

2553

Age (days ago)

2554

Last active (days ago)

List overview

Download

10 comments

5 participants

participants (5)

Conal Elliott
David Feuer
Joe Hendrix
Richard Eisenberg
Simon Peyton Jones