Re: [commit: packages/base] master: Add functions to compare Nat and Symbol types for equality. (c5c8c4d)
Iavor, this is great! Just out of curiosity, you import TestEquality but never reference it. Is this an oversight, should I nuke it? Cheers, Gabor On 1/4/14, git@git.haskell.org <git@git.haskell.org> wrote:
Repository : ssh://git@git.haskell.org/base
On branch : master Link : http://ghc.haskell.org/trac/ghc/changeset/c5c8c4dfbdc8493bcfaa804751eff2a9a4...
---------------------------------------------------------------
commit c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a Author: Iavor S. Diatchki <diatchki@galois.com> Date: Fri Jan 3 15:11:34 2014 -0800
Add functions to compare Nat and Symbol types for equality.
---------------------------------------------------------------
c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a GHC/TypeLits.hs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs index f3ba70e..129beb3 100644 --- a/GHC/TypeLits.hs +++ b/GHC/TypeLits.hs @@ -26,6 +26,8 @@ module GHC.TypeLits , KnownSymbol, symbolVal , SomeNat(..), SomeSymbol(..) , someNatVal, someSymbolVal + , sameNat, sameSymbol +
-- * Functions on type nats , type (<=), type (<=?), type (+), type (*), type (^), type (-) @@ -40,7 +42,8 @@ import GHC.Read(Read(..)) import GHC.Prim(magicDict) import Data.Maybe(Maybe(..)) import Data.Proxy(Proxy(..)) -import Data.Type.Equality(type (==)) +import Data.Type.Equality(type (==), TestEquality(..), (:~:)(Refl)) +import Unsafe.Coerce(unsafeCoerce)
-- | (Kind) This is the kind of type-level natural numbers. data Nat @@ -167,6 +170,23 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat type family (m :: Nat) - (n :: Nat) :: Nat
+-------------------------------------------------------------------------------- + +-- | We either get evidence that this function was instantiated with the +-- same type-level numbers, or 'Nothing'. +sameNat :: (KnownNat a, KnownNat b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameNat x y + | natVal x == natVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | We either get evidence that this function was instantiated with the +-- same type-level symbols, or 'Nothing'. +sameSymbol :: (KnownSymbol a, KnownSymbol b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameSymbol x y + | symbolVal x == symbolVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing
-------------------------------------------------------------------------------- -- PRIVATE: @@ -187,3 +207,4 @@ withSSymbol :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b withSSymbol f x y = magicDict (WrapS f) x y
+
_______________________________________________ ghc-commits mailing list ghc-commits@haskell.org http://www.haskell.org/mailman/listinfo/ghc-commits
Hi, oh yes, I was going to add the instance and then I realized it doesn't work. Please feel free to fix. Thanks! -Iavor On Fri, Jan 3, 2014 at 3:25 PM, Gabor Greif <ggreif@gmail.com> wrote:
Iavor,
this is great! Just out of curiosity, you import TestEquality but never reference it. Is this an oversight, should I nuke it?
Cheers,
Gabor
On 1/4/14, git@git.haskell.org <git@git.haskell.org> wrote:
Repository : ssh://git@git.haskell.org/base
On branch : master Link :
http://ghc.haskell.org/trac/ghc/changeset/c5c8c4dfbdc8493bcfaa804751eff2a9a4...
---------------------------------------------------------------
commit c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a Author: Iavor S. Diatchki <diatchki@galois.com> Date: Fri Jan 3 15:11:34 2014 -0800
Add functions to compare Nat and Symbol types for equality.
---------------------------------------------------------------
c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a GHC/TypeLits.hs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs index f3ba70e..129beb3 100644 --- a/GHC/TypeLits.hs +++ b/GHC/TypeLits.hs @@ -26,6 +26,8 @@ module GHC.TypeLits , KnownSymbol, symbolVal , SomeNat(..), SomeSymbol(..) , someNatVal, someSymbolVal + , sameNat, sameSymbol +
-- * Functions on type nats , type (<=), type (<=?), type (+), type (*), type (^), type (-) @@ -40,7 +42,8 @@ import GHC.Read(Read(..)) import GHC.Prim(magicDict) import Data.Maybe(Maybe(..)) import Data.Proxy(Proxy(..)) -import Data.Type.Equality(type (==)) +import Data.Type.Equality(type (==), TestEquality(..), (:~:)(Refl)) +import Unsafe.Coerce(unsafeCoerce)
-- | (Kind) This is the kind of type-level natural numbers. data Nat @@ -167,6 +170,23 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat type family (m :: Nat) - (n :: Nat) :: Nat
+--------------------------------------------------------------------------------
+ +-- | We either get evidence that this function was instantiated with the +-- same type-level numbers, or 'Nothing'. +sameNat :: (KnownNat a, KnownNat b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameNat x y + | natVal x == natVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | We either get evidence that this function was instantiated with the +-- same type-level symbols, or 'Nothing'. +sameSymbol :: (KnownSymbol a, KnownSymbol b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameSymbol x y + | symbolVal x == symbolVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing
--------------------------------------------------------------------------------
-- PRIVATE: @@ -187,3 +207,4 @@ withSSymbol :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b withSSymbol f x y = magicDict (WrapS f) x y
+
_______________________________________________ ghc-commits mailing list ghc-commits@haskell.org http://www.haskell.org/mailman/listinfo/ghc-commits
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
On 1/4/14, Iavor Diatchki <iavor.diatchki@gmail.com> wrote:
Hi, oh yes, I was going to add the instance and then I realized it doesn't work. Please feel free to fix. Thanks!
Done: http://ghc.haskell.org/trac/ghc/changeset/b62f687e23d90c2ff4536e4e7788e5d9ac... Cheers, Gabor
-Iavor
On Fri, Jan 3, 2014 at 3:25 PM, Gabor Greif <ggreif@gmail.com> wrote:
Iavor,
this is great! Just out of curiosity, you import TestEquality but never reference it. Is this an oversight, should I nuke it?
Cheers,
Gabor
On 1/4/14, git@git.haskell.org <git@git.haskell.org> wrote:
Repository : ssh://git@git.haskell.org/base
On branch : master Link :
http://ghc.haskell.org/trac/ghc/changeset/c5c8c4dfbdc8493bcfaa804751eff2a9a4...
---------------------------------------------------------------
commit c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a Author: Iavor S. Diatchki <diatchki@galois.com> Date: Fri Jan 3 15:11:34 2014 -0800
Add functions to compare Nat and Symbol types for equality.
---------------------------------------------------------------
c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a GHC/TypeLits.hs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs index f3ba70e..129beb3 100644 --- a/GHC/TypeLits.hs +++ b/GHC/TypeLits.hs @@ -26,6 +26,8 @@ module GHC.TypeLits , KnownSymbol, symbolVal , SomeNat(..), SomeSymbol(..) , someNatVal, someSymbolVal + , sameNat, sameSymbol +
-- * Functions on type nats , type (<=), type (<=?), type (+), type (*), type (^), type (-) @@ -40,7 +42,8 @@ import GHC.Read(Read(..)) import GHC.Prim(magicDict) import Data.Maybe(Maybe(..)) import Data.Proxy(Proxy(..)) -import Data.Type.Equality(type (==)) +import Data.Type.Equality(type (==), TestEquality(..), (:~:)(Refl)) +import Unsafe.Coerce(unsafeCoerce)
-- | (Kind) This is the kind of type-level natural numbers. data Nat @@ -167,6 +170,23 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat type family (m :: Nat) - (n :: Nat) :: Nat
+--------------------------------------------------------------------------------
+ +-- | We either get evidence that this function was instantiated with the +-- same type-level numbers, or 'Nothing'. +sameNat :: (KnownNat a, KnownNat b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameNat x y + | natVal x == natVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | We either get evidence that this function was instantiated with the +-- same type-level symbols, or 'Nothing'. +sameSymbol :: (KnownSymbol a, KnownSymbol b) => + Proxy a -> Proxy b -> Maybe (a :~: b) +sameSymbol x y + | symbolVal x == symbolVal y = Just (unsafeCoerce Refl) + | otherwise = Nothing
--------------------------------------------------------------------------------
-- PRIVATE: @@ -187,3 +207,4 @@ withSSymbol :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b withSSymbol f x y = magicDict (WrapS f) x y
+
_______________________________________________ ghc-commits mailing list ghc-commits@haskell.org http://www.haskell.org/mailman/listinfo/ghc-commits
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
participants (2)
-
Gabor Greif -
Iavor Diatchki