Make sameNat proxy-polymorphic

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

Make sameNat proxy-polymorphic

Andrew Lelechenko
Hi all,

Currently base:GHC.TypeNats.sameNat is implemented as follows:

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
  | natVal x == natVal y = Just (unsafeCoerce Refl)
  | otherwise = Nothing

There are applications, when more flexibility is desirable. I propose to change sameNat's type to

sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

It does not require any changes in the implementation, because natVal is already "proxy-polymorphic":

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

Best regards,
Andrew
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Make sameNat proxy-polymorphic

chessai .
+1

On Tue, Aug 13, 2019, 7:32 PM Andrew Lelechenko <[hidden email]> wrote:
Hi all,

Currently base:GHC.TypeNats.sameNat is implemented as follows:

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
  | natVal x == natVal y = Just (unsafeCoerce Refl)
  | otherwise = Nothing

There are applications, when more flexibility is desirable. I propose to change sameNat's type to

sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

It does not require any changes in the implementation, because natVal is already "proxy-polymorphic":

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

Best regards,
Andrew
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: Make sameNat proxy-polymorphic

Eric Mertens
In reply to this post by Andrew Lelechenko
While we’re fixing that, let’s also fix sameSymbol.

> On Aug 13, 2019, at 4:32 PM, Andrew Lelechenko <[hidden email]> wrote:
>
> Hi all,
>
> Currently base:GHC.TypeNats.sameNat is implemented as follows:
>
> sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
> sameNat x y
>  | natVal x == natVal y = Just (unsafeCoerce Refl)
>  | otherwise = Nothing
>
> There are applications, when more flexibility is desirable. I propose to change sameNat's type to
>
> sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
>
> It does not require any changes in the implementation, because natVal is already "proxy-polymorphic":
>
> natVal :: forall n proxy. KnownNat n => proxy n -> Natural
>
> Best regards,
> Andrew
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: Make sameNat proxy-polymorphic

Carter Schonwald
+1 on all of the above, I generally find my proxy code is nicest when i'm polymoprophic over the prox :) 

On Wed, Aug 14, 2019 at 12:45 PM Eric Mertens <[hidden email]> wrote:
While we’re fixing that, let’s also fix sameSymbol.

> On Aug 13, 2019, at 4:32 PM, Andrew Lelechenko <[hidden email]> wrote:
>
> Hi all,
>
> Currently base:GHC.TypeNats.sameNat is implemented as follows:
>
> sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
> sameNat x y
>  | natVal x == natVal y = Just (unsafeCoerce Refl)
>  | otherwise = Nothing
>
> There are applications, when more flexibility is desirable. I propose to change sameNat's type to
>
> sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
>
> It does not require any changes in the implementation, because natVal is already "proxy-polymorphic":
>
> natVal :: forall n proxy. KnownNat n => proxy n -> Natural
>
> Best regards,
> Andrew
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries