Repository : ssh://darcs.haskell.org//srv/darcs/packages/base On branch : master
http://hackage.haskell.org/trac/ghc/changeset/85bda3d6e36fb8b3d7121ccc01c8ccfc3942431f >--------------------------------------------------------------- commit 85bda3d6e36fb8b3d7121ccc01c8ccfc3942431f Author: Iavor S. Diatchki <[email protected]> Date: Sat Dec 22 15:22:43 2012 -0800 Add functions that compare singletons for equality (with evidence) >--------------------------------------------------------------- GHC/TypeLits.hs | 40 ++++++++++++++++++++++++++++++++++++++++ 1 files changed, 40 insertions(+), 0 deletions(-) diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs index 50a5c86..ed1f205 100644 --- a/GHC/TypeLits.hs +++ b/GHC/TypeLits.hs @@ -29,10 +29,14 @@ module GHC.TypeLits , type (<=), type (<=?), type (+), type (*), type (^) , type (-) + -- * Comparing for equality + , type (:~:) (..), eqSingNat, eqSingSym + -- * Destructing type-nat singletons. , isZero, IsZero(..) , isEven, IsEven(..) + -- * Matching on type-nats , Nat1(..), FromNat1 @@ -215,4 +219,40 @@ type family FromNat1 (n :: Nat1) :: Nat type instance FromNat1 Zero = 0 type instance FromNat1 (Succ n) = 1 + FromNat1 n +-------------------------------------------------------------------------------- + +-- | A type that provides evidence for equality between two types. +data (:~:) :: k -> k -> * where + Refl :: a :~: a + +instance Show (a :~: b) where + show Refl = "Refl" + +{- | Check if two type-natural singletons of potentially different types +are indeed the same, by comparing their runtime representations. + +WARNING: in combination with `unsafeSingNat` this may lead to unsoudness: + +> eqSingNat (sing :: Sing 1) (unsafeSingNat 1 :: Sing 2) +> == Just (Refl :: 1 :~: 2) +-} + +eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n) +eqSingNat x y + | fromSing x == fromSing y = Just (unsafeCoerce Refl) + | otherwise = Nothing + + +{- | Check if two symbol singletons of potentially different types +are indeed the same, by comparing their runtime representations. +WARNING: in combination with `unsafeSingSymbol` this may lead to unsoudness +(see `eqSingNat` for an example). +-} + +eqSingSym:: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n) +eqSingSym x y + | fromSing x == fromSing y = Just (unsafeCoerce Refl) + | otherwise = Nothing + + _______________________________________________ Cvs-libraries mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-libraries
