[commit: packages/base] master: Add functions to compare Nat and Symbol types for equality. (c5c8c4d)

[Gabor Greif]

On 1/4/14, Iavor Diatchki <iavor.diatchki at 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/b62f687e23d90c2ff4536e4e7788e5d9acb2b66c/base

Cheers,

    Gabor

> -Iavor
>
>
> On Fri, Jan 3, 2014 at 3:25 PM, Gabor Greif <ggreif at 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 at git.haskell.org <git at git.haskell.org> wrote:
>> > Repository : ssh://git@git.haskell.org/base
>> >
>> > On branch  : master
>> > Link       :
>> >
>> http://ghc.haskell.org/trac/ghc/changeset/c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a/base
>> >
>> >>---------------------------------------------------------------
>> >
>> > commit c5c8c4dfbdc8493bcfaa804751eff2a9a41cc07a
>> > Author: Iavor S. Diatchki <diatchki at 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 at haskell.org
>> > http://www.haskell.org/mailman/listinfo/ghc-commits
>> >
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>