singletons 0.8.2 → 0.8.3
raw patch · 6 files changed
+92/−42 lines, 6 files
Files
- CHANGES +10/−0
- Data/Singletons.hs +30/−11
- Data/Singletons/Singletons.hs +15/−13
- Data/Singletons/TypeRepStar.hs +5/−5
- README +31/−12
- singletons.cabal +1/−1
CHANGES view
@@ -1,6 +1,16 @@ Changelog for singletons project ================================ +0.8.3+-----++Update to work with latest version of GHC (7.7.20121031).++Removed use of Any to simulate kind classes; now using KindOf and OfKind+from GHC.TypeLits.++Made compatible with GHC.TypeLits.+ 0.8.2 -----
Data/Singletons.hs view
@@ -13,13 +13,14 @@ {-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TemplateHaskell, DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses, FlexibleContexts, RankNTypes, UndecidableInstances,- FlexibleInstances, ScopedTypeVariables+ FlexibleInstances, ScopedTypeVariables, CPP #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Data.Singletons (+ OfKind(..), Sing(..), SingI(..), SingE(..), SingRep, KindOf, Demote, Any,- Demote, Sing(..), SingI(sing), SingE(fromSing), SingRep, (:==), (:==:),+ (:==), (:==:), SingInstance(..), SingKind(singInstance), sTrue, sFalse, SBool, sNothing, sJust, SMaybe, sLeft, sRight, SEither, sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7,@@ -36,27 +37,45 @@ import Data.Singletons.Singletons import Data.Singletons.Promote import Language.Haskell.TH-import GHC.Exts import Data.Singletons.Util+import GHC.Exts (Any) +#if __GLASGOW_HASKELL__ >= 707++import GHC.TypeLits ( OfKind(..), Sing(..), SingI(..), SingE(..),+ SingRep, KindOf, Demote )++#else++-- Kind-level proxy+data OfKind (k :: *) = KindParam++-- Access the kind of a type variable+type KindOf (a :: k) = (KindParam :: OfKind k)+ -- Declarations of singleton structures data family Sing (a :: k) class SingI (a :: k) where sing :: Sing a-class SingE (a :: k) where- type Demote a :: *- fromSing :: Sing a -> Demote (Any :: k)+class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where+ type DemoteRep kparam :: *+ fromSing :: Sing (a :: k) -> DemoteRep kparam -- SingRep is a synonym for (SingI, SingE)-class (SingI a, SingE a) => SingRep a-instance (SingI a, SingE a) => SingRep a+class (SingI a, SingE (KindOf a)) => SingRep (a :: k)+instance (SingI a, SingE (KindOf a)) => SingRep (a :: k) +-- Abbreviation for DemoteRep+type Demote (a :: k) = DemoteRep (KindParam :: OfKind k)++#endif+ type family (a :: k) :==: (b :: k) :: Bool type a :== b = a :==: b -- :== and :==: are synonyms data SingInstance (a :: k) where SingInstance :: SingRep a => SingInstance a-class (b ~ Any) => SingKind (b :: k) where+class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where singInstance :: forall (a :: k). Sing a -> SingInstance a -- provide a few useful singletons...@@ -86,7 +105,7 @@ type a :/= b = a :/=: b -- the singleton analogue of @Eq@-class (t ~ Any) => SEq (t :: k) where+class (kparam ~ KindParam) => SEq (kparam :: OfKind k) where (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b) (%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b) (%:==) = (%==%)@@ -110,7 +129,7 @@ type instance (h ': t) :==: '[] = False type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t') -instance SEq (Any :: k) => SEq (Any :: [k]) where+instance SEq (KindParam :: OfKind k) => SEq (KindParam :: OfKind [k]) where SNil %==% SNil = STrue SNil %==% (SCons _ _) = SFalse (SCons _ _) %==% SNil = SFalse
Data/Singletons/Singletons.hs view
@@ -32,14 +32,14 @@ singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName, demoteName, singKindClassName, singInstanceMethName, singInstanceName, sEqClassName, sEqMethName, sconsName, snilName, smartSconsName,- smartSnilName, sIfName, undefinedName :: Name+ smartSnilName, sIfName, undefinedName, kindParamName, ofKindName :: Name singFamilyName = mkName "Sing" isSingletonName = mkName "SingI" forgettableName = mkName "SingE" comboClassName = mkName "SingRep" witnessName = mkName "sing" forgetName = mkName "fromSing"-demoteName = mkName "Demote"+demoteName = mkName "DemoteRep" singKindClassName = mkName "SingKind" singInstanceMethName = mkName "singInstance" singInstanceName = mkName "SingInstance"@@ -51,6 +51,8 @@ smartSnilName = mkName "sNil" sIfName = mkName "sIf" undefinedName = mkName "undefined"+kindParamName = mkName "KindParam"+ofKindName = mkName "OfKind" mkTupleName :: Int -> Name mkTupleName n = mkName $ "STuple" ++ (show n)@@ -59,7 +61,7 @@ singFamily = ConT singFamilyName singKindConstraint :: Kind -> Pred-singKindConstraint k = ClassP singKindClassName [SigT anyType k]+singKindConstraint k = ClassP singKindClassName [kindParam k] singInstanceMeth :: Exp singInstanceMeth = VarE singInstanceMethName@@ -76,9 +78,6 @@ demote :: Type demote = ConT demoteName -anyType :: Type-anyType = ConT anyTypeName- singDataConName :: Name -> Name singDataConName nm = case nameBase nm of "[]" -> snilName@@ -108,6 +107,9 @@ singVal :: Name -> Exp singVal = VarE . singValName +kindParam :: Kind -> Type+kindParam k = SigT (ConT kindParamName) (AppT (ConT ofKindName) k)+ -- generate singleton definitions from an ADT genSingletons :: [Name] -> Q [Dec] genSingletons names = do@@ -285,7 +287,7 @@ let singKindInst = InstanceD [] (AppT (ConT singKindClassName)- (SigT anyType k))+ (kindParam k)) [FunD singInstanceMethName (map mkSingInstanceClause ctors')] @@ -293,10 +295,10 @@ let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ] sEqMethClauses <- mapM mkEqMethClause ctorPairs let sEqInst =- InstanceD (map (\k -> ClassP sEqClassName [SigT anyType k])+ InstanceD (map (\k -> ClassP sEqClassName [kindParam k]) (getBareKinds ctors')) (AppT (ConT sEqClassName)- (SigT anyType k))+ (kindParam k)) [FunD sEqMethName sEqMethClauses] -- e.g. type SNat (a :: Nat) = Sing a@@ -309,10 +311,10 @@ forgetClauses <- mapM mkForgetClause ctors let singEInst = InstanceD []- (AppT (ConT forgettableName) (SigT a k))- [TySynInstD demoteName [a]+ (AppT (ConT forgettableName) (kindParam k))+ [TySynInstD demoteName [kindParam k] (foldType (ConT name)- (map (\kv -> AppT demote (SigT anyType (VarT kv)))+ (map (\kv -> AppT demote (kindParam (VarT kv))) tvbNames)), FunD forgetName forgetClauses]@@ -437,7 +439,7 @@ -- left of an odd number of arrows) let polykinds = extractPolyKinds (not pos) k1 return (\f -> ForallT [KindedTV t k1]- (map (\k -> ClassP singKindClassName [SigT anyType k]) polykinds)+ (map (\k -> ClassP singKindClassName [kindParam k]) polykinds) (AppT (AppT ArrowT (sty1 (VarT t))) (sty2 (AppT f (VarT t))))) where extractPolyKinds :: Bool -> Kind -> [Kind]
Data/Singletons/TypeRepStar.hs view
@@ -9,7 +9,7 @@ -} {-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,- GADTs, UndecidableInstances, ScopedTypeVariables #-}+ GADTs, UndecidableInstances, ScopedTypeVariables, DataKinds #-} module Data.Singletons.TypeRepStar where @@ -24,8 +24,8 @@ instance Typeable a => SingI (a :: *) where sing = STypeRep-instance SingE (a :: *) where- type Demote a = TypeRep- fromSing STypeRep = typeOf (undefined :: a)-instance SingKind (Any :: *) where+instance SingE (KindParam :: OfKind *) where+ type DemoteRep (KindParam :: OfKind *) = TypeRep+ fromSing (STypeRep :: Sing a) = typeOf (undefined :: a)+instance SingKind (KindParam :: OfKind *) where singInstance STypeRep = SingInstance
README view
@@ -109,10 +109,29 @@ Definitions used to support singletons -------------------------------------- -Please refer to the paper cited above for a more in-dpeth explanation of these+Please refer to the paper cited above for a more in-depth explanation of these definitions. +-----+NOTE: The original paper used a trick with the GHC primitive 'Any' to simulate+kind classes and to perform other shenanigans. 'Any' is like undefined at the+type level. GHC has evolved to prevent pattern-matching on 'Any', which is a+Good Thing. This means that some of singletons's uses of 'Any' were invalid.+These were replaced with a kind-level proxy, defined thus: +data OfKind (k :: *) = KindParam+type KindOf (a :: k) = (KindParam :: OfKind k)++The parameter must be explicitly kinded to * to prevent polymorphism, because+only monomorphic types are promoted to kinds. This definition should only be+used at the kind level.+-----++Many of the definitions were developed in tandem with Iavor Diatchki, the+maintainer of type-level literals in GHC. In GHC 7.7+, the singletons library+imports many of these definitions from GHC.TypeLits.++ data family Sing (a :: k) The data family of singleton types. A new instance of this data family is@@ -126,21 +145,21 @@ an explicit singleton value. -class SingE (a :: k) where- type Demote a :: *- fromSing :: Sing a -> Demote (Any :: k)+class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where+ type DemoteRep kparam :: *+ fromSing :: Sing (a :: k) -> DemoteRep kparam This class is used to convert a singleton value back to a value in the original, unrefined ADT. The 'fromSing' method converts, say, a-singleton @Nat@ back to an ordinary @Nat@. The 'Demote' associated-kind-indexed type family maps, for example, types of the kind @Nat@+singleton @Nat@ back to an ordinary @Nat@. The 'DemoteRep' associated+kind-indexed type family maps a proxy of the kind @Nat@ back to the type @Nat@. -class (SingI a, SingE a) => SingRep a-instance (SingI a, SingE a) => SingRep a+class (SingI a, SingE (KindOf a)) => SingRep (a :: k)+instance (SingI a, SingE (KindOf a)) => SingRep (a :: k) -'SingRep' is a synonym for @('SingI' a, 'SingE' a)@.+'SingRep' is a synonym for @('SingI' a, 'SingE' (KindOf a))@. type family (a :: k) :==: (b :: k) :: Bool@@ -154,15 +173,15 @@ data SingInstance (a :: k) where SingInstance :: SingRep a => SingInstance a-class (b ~ Any) => SingKind (b :: k) where+class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where singInstance :: forall (a :: k). Sing a -> SingInstance a The 'SingKind' class allows for easy access to implicit parameters. The intuition here is that for any kind @k@ with an associated singleton definition,-@SingKind (Any :: k)@ is defined.+@SingKind (KindParam :: OfKind k)@ is defined. -class (t ~ Any) => SEq (t :: k) where+class (kparam ~ KindParam) => SEq (kparam :: OfKind k) where (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b) (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
singletons.cabal view
@@ -1,5 +1,5 @@ name: singletons-version: 0.8.2+version: 0.8.3 cabal-version: >= 1.8 synopsis: A framework for generating singleton types homepage: http://www.cis.upenn.edu/~eir/packages/singletons