diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -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 ----- diff --git a/Data/Singletons.hs b/Data/Singletons.hs --- a/Data/Singletons.hs +++ b/Data/Singletons.hs @@ -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 diff --git a/Data/Singletons/Singletons.hs b/Data/Singletons/Singletons.hs --- a/Data/Singletons/Singletons.hs +++ b/Data/Singletons/Singletons.hs @@ -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] diff --git a/Data/Singletons/TypeRepStar.hs b/Data/Singletons/TypeRepStar.hs --- a/Data/Singletons/TypeRepStar.hs +++ b/Data/Singletons/TypeRepStar.hs @@ -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 diff --git a/README b/README --- a/README +++ b/README @@ -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) diff --git a/singletons.cabal b/singletons.cabal --- a/singletons.cabal +++ b/singletons.cabal @@ -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