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

Iavor Diatchki iavor.diatchki at gmail.com
Sat Jan 4 01:44:20 UTC 2014


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 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140103/a3923ac2/attachment.html>


More information about the ghc-devs mailing list