RFC: Singleton equality witnesses
Gabor Greif <[email protected]>
| Newsgroups | gmane.comp.lang.haskell.cvs.ghc |
|---|---|
| Message-ID | <CAK-hX0nJZMG1t9NHw_acu+HAy8rJkUC7gVAgvPNrAketgqywqw@mail.gmail.com> |
Hi all!
After encouragement from Iavor on G+, here is a patch that implements
a class method for singleton type equality witnesses in a generic way.
Please comment on two things:
- is this a good approach?
- how can we avoid abuse of SingEq (as it is type polymorphic, can this harm?)
- (possibly) bikeshedding on names.
Cheers and thanks,
Gabor
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
TypeLits.hs.patch
(application/octet-stream, 1.7 KB)
diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 50a5c86..cf04658 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -25,6 +25,9 @@ module GHC.TypeLits
-- * Working with singletons
, withSing, singThat
+ -- * Singleton type equality witness
+ , SingEq(..)
+
-- * Functions on type nats
, type (<=), type (<=?), type (+), type (*), type (^)
, type (-)
@@ -50,6 +53,7 @@ import Unsafe.Coerce(unsafeCoerce)
import Data.Bits(testBit,shiftR)
import Data.Maybe(Maybe(..))
import Data.List((++))
+import Control.Monad (guard, return, (>>))
-- | (Kind) A kind useful for passing kinds as parameters.
data OfKind (a :: *) = KindParam
@@ -123,17 +127,27 @@ and not their type---all types of a given kind are processed by the
same instances.
-}
+data SingEq :: k -> k -> * where
+ SingEq :: SingEq s s
+
class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
type DemoteRep kparam :: *
fromSing :: Sing (a :: k) -> DemoteRep kparam
+ type SameSing kparam :: k -> k -> *
+ type SameSing kparam = SingEq
+ sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
instance SingE (KindParam :: OfKind Nat) where
type DemoteRep (KindParam :: OfKind Nat) = Integer
fromSing (SNat n) = n
+ sameSing a b = do guard $ fromSing a == fromSing b
+ return $ unsafeCoerce SingEq
instance SingE (KindParam :: OfKind Symbol) where
type DemoteRep (KindParam :: OfKind Symbol) = String
fromSing (SSym s) = s
+ sameSing a b = do guard $ fromSing a == fromSing b
+ return $ unsafeCoerce SingEq
{- | A convenient name for the type used to representing the values
for a particular singleton family. For example, @Demote 2 ~ Integer@,