Natural number comparisons with evidence

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Natural number comparisons with evidence

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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

David Feuer
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Conal Elliott
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:
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Conal Elliott
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:
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:
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

David Feuer
In reply to this post by Conal Elliott
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Conal Elliott
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Richard Eisenberg-4
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
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Conal Elliott
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
Reply | Threaded
Open this post in threaded view
|

RE: Natural number comparisons with evidence

Haskell - Glasgow-haskell-users mailing list
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
Sent: 24 May 2018 00:39
To: [hidden email]
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

 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

Conal Elliott
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:

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
Sent: 24 May 2018 00:39
To: [hidden email]
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

 



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Natural number comparisons with evidence

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