Re: Natural number comparisons with evidence

[Joe Hendrix]

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



signature.asc
Description: Message signed with OpenPGP
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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 
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
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

RE: Natural number comparisons with evidence

[Simon Peyton Jones via Glasgow-haskell-users]

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

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

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

Re: Natural number comparisons with evidence

[Richard Eisenberg]

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

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

Re: Natural number comparisons with evidence

[David Feuer]

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

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  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
>>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

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