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

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Gabor Greif-2
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 at 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
>

Reply | Threaded
Open this post in threaded view
|

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

Iavor Diatchki
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 at 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>

Reply | Threaded
Open this post in threaded view
|

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

Gabor Greif-2
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 at 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
>>
>