+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
While we’re fixing that, let’s also fix sameSymbol.
On Aug 13, 2019, at 4:32 PM, Andrew Lelechenko < andrew.lelechenko@gmail.com> 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 Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries