From f19184ed9e061bd2574922994dc1e4736744b25e Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Fri, 18 Mar 2016 09:10:06 -0400 Subject: wip Converted to singletons. Type level functions not updated yet. --- src/Propellor/Types/Target.hs | 202 ++++++++++++++++++++++++------------------ 1 file changed, 114 insertions(+), 88 deletions(-) (limited to 'src') diff --git a/src/Propellor/Types/Target.hs b/src/Propellor/Types/Target.hs index 8b17d32f..4f781f55 100644 --- a/src/Propellor/Types/Target.hs +++ b/src/Propellor/Types/Target.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, AllowAmbiguousTypes, TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables, GADTs #-} module Propellor.Types.Target ( {- @@ -28,126 +28,144 @@ import Data.Typeable import Data.String import Data.List -data Property proptypes = Property proptypes (IO ()) - -mkProperty :: proptypes -> IO () -> Property proptypes -mkProperty proptypes a = Property proptypes a - -{- - -mkProperty' :: proptypes -> (OuterPropTypes proptypes -> IO ()) -> Property proptypes -mkProperty' target@l a = Property target (a (OuterPropTypes l)) - -data OuterPropTypes (proptypes :: PropTypes) = OuterPropTypes PropTypes - --- | Use `mkProperty'` to get the `OuterTarget`. Only properties whose --- targets are a superset of the outer targets can be ensured. -ensureProperty - :: ((innertargets `NotSupersetTargets` outertargets) ~ CanCombineTargets) - => OuterTarget outertargets - -> Property (Targeting innertargets) - -> IO () -ensureProperty outertarget (Property innertarget a) = a - --- | Changes the target of a property. --- --- This can only tighten the target list to contain fewer targets. -target - :: (combinedtarget ~ IntersectTarget oldtarget newtarget, CannotCombineTargets oldtarget newtarget combinedtarget ~ CanCombineTargets) - => Targeting newtarget - -> Property (Targeting oldtarget) - -> Property (Targeting combinedtarget) -target newtarget (Property oldtarget a) = - Property (intersectTarget oldtarget newtarget) a - --- | Picks one of the two input properties to use, --- depending on the targeted OS. --- --- If both input properties support the targeted OS, then the --- first will be used. -orProperty - :: Property (Targeting a) - -> Property (Targeting b) - -> Property (Targeting (UnionTarget a b)) -orProperty a@(Property ta ioa) b@(Property tb iob) = - Property (unionTargets ta tb) io - where - -- TODO pick with of ioa or iob to use based on final OS of - -- system being run on. - io = undefined - ----- DEMO ---------- + -- Intentionally a type error! :) --foo :: Property (Targeting '[OSDebian, OSFreeBSD]) --foo = Property supportedos $ do -- ensureProperty supportedos jail -- where supportedos = unionTargets debian freeBSD -foo :: Property (Targeting '[OSFreeBSD]) -foo = mkProperty' freeBSD $ \t -> do - ensureProperty t jail - +{- bar :: Property (Targeting '[OSDebian, OSFreeBSD]) bar = aptinstall `orProperty` jail +-} + +foo :: Property FreeBSDOnly +foo = mkProperty' $ \t -> do + ensureProperty t jail + aptinstall :: Property DebianOnly -aptinstall = mkProperty debian $ do +aptinstall = mkProperty $ do return () -jail :: Property FreeBSDOnly -jail = mkProperty freeBSD $ do +jail :: Property (HasInfo :+: FreeBSDOnly) +jail = mkProperty $ do return () + ----- END DEMO ---------- --} +data Property proptypes = Property proptypes (IO ()) --- | A Target system, where a Property is indended to be used. -data Target = OSDebian | OSBuntish | OSFreeBSD +mkProperty :: Sing l => IO () -> Property (WithTypes l) +mkProperty = mkProperty' . const + +mkProperty' :: Sing l => (OuterPropTypes l -> IO ()) -> Property (WithTypes l) +mkProperty' a = + let p = Property sing (a (outerPropTypes p)) + in p + +data OS = OSDebian | OSBuntish | OSFreeBSD deriving (Show, Eq) --- | A property has a list of associated PropType's data PropType - = Targeting Target -- ^ A target OS of a Property - | HasInfo -- ^ Indicates that a Property has associated Info + = Targeting OS -- ^ A target OS of a Property + | WithInfo -- ^ Indicates that a Property has associated Info deriving (Show, Eq) -data PropTypes (proptypes :: [PropType]) = PropTypes [PropType] - -type UnixLike = PropTypes '[Targeting OSDebian, Targeting OSBuntish, Targeting OSFreeBSD] +-- | Any unix-like system +type UnixLike = WithTypes '[Targeting OSDebian, Targeting OSBuntish, Targeting OSFreeBSD] +type DebianOnly = WithTypes '[Targeting OSDebian] +type BuntishOnly = WithTypes '[Targeting OSBuntish] +type FreeBSDOnly = WithTypes '[Targeting OSFreeBSD] -unixLike :: UnixLike -unixLike = PropTypes [Targeting OSDebian, Targeting OSBuntish, Targeting OSFreeBSD] +type HasInfo = WithTypes '[WithInfo] -type DebianOnly = PropTypes '[Targeting OSDebian] +data family WithTypes (x :: k) -debian :: DebianOnly -debian = targeting OSDebian +class Sing t where + -- Constructor for a singleton WithTypes list. + sing :: WithTypes t -type BuntishOnly = PropTypes '[Targeting OSBuntish] +data instance WithTypes (x :: [k]) where + Nil :: WithTypes '[] + Cons :: WithTypes x -> WithTypes xs -> WithTypes (x ': xs) -buntish :: BuntishOnly -buntish = targeting OSBuntish +instance (Sing x, Sing xs) => Sing (x ': xs) where sing = Cons sing sing +instance Sing '[] where sing = Nil -type FreeBSDOnly = PropTypes '[Targeting OSFreeBSD] +-- This boilerplatw would not be needed if the singletons library were +-- used. However, we're targeting too old a version of ghc to use it yet. +data instance WithTypes (x :: PropType) where + OSDebianS :: WithTypes ('Targeting OSDebian) + OSBuntishS :: WithTypes ('Targeting OSBuntish) + OSFreeBSDS :: WithTypes ('Targeting OSFreeBSD) + WithInfoS :: WithTypes 'WithInfo +instance Sing ('Targeting OSDebian) where sing = OSDebianS +instance Sing ('Targeting OSBuntish) where sing = OSBuntishS +instance Sing ('Targeting OSFreeBSD) where sing = OSFreeBSDS +instance Sing 'WithInfo where sing = WithInfoS -freeBSD :: FreeBSDOnly -freeBSD = targeting OSFreeBSD +-- | Convenience type operator to combine two WithTypes lists. +-- +-- For example, to add HasInfo to the DebianOnly list: +-- +-- > HasInfo :+: DebianOnly +-- +-- Which is shorthand for this type: +-- +-- > WithTypes '[WithInfo, Targeting OSDebian] +type family a :+: b :: ab +type instance (WithTypes a) :+: (WithTypes b) = WithTypes (Concat a b) -targeting :: Target -> PropTypes l -targeting o = PropTypes [Targeting o] +type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] +type instance Concat '[] bs = bs +type instance Concat (a ': as) bs = a ': (Concat as bs) -foo :: PropTypes (HasInfo :+: DebianOnly) -foo = HasInfo `also` debian +newtype OuterPropTypes l = OuterPropTypes (WithTypes l) -also :: (l' ~ (:+:) t (PropTypes l)) => PropType -> (PropTypes l) -> PropTypes l' -p `also` PropTypes l = PropTypes (p:l) +outerPropTypes :: Property (WithTypes l) -> OuterPropTypes l +outerPropTypes (Property proptypes _) = OuterPropTypes proptypes --- | Add a PropType to a PropTypes -type family (p :: PropType) :+: l :: l2 -type instance p :+: (PropTypes l) = PropTypes (p ': l) +-- | Use `mkProperty''` to get the `OuterPropTypes`. Only properties whose +-- PropTypes are a superset of the OuterPropTypes can be ensured. +ensureProperty + :: ((inner `NotSupersetTargets` outer) ~ CanCombineTargets) + => OuterPropTypes outer + -> Property inner + -> IO () +ensureProperty (OuterPropTypes outerproptypes) (Property innerproptypes a) = a {- +-- | Changes the target of a property. +-- +-- This can only tighten the target list to contain fewer targets. +target + :: (combinedtarget ~ IntersectTarget oldtarget newtarget, CannotCombineTargets oldtarget newtarget combinedtarget ~ CanCombineTargets) + => Targeting newtarget + -> Property (Targeting oldtarget) + -> Property (Targeting combinedtarget) +target newtarget (Property oldtarget a) = + Property (intersectTarget oldtarget newtarget) a + +-- | Picks one of the two input properties to use, +-- depending on the targeted OS. +-- +-- If both input properties support the targeted OS, then the +-- first will be used. +orProperty + :: Property (Targeting a) + -> Property (Targeting b) + -> Property (Targeting (UnionTarget a b)) +orProperty a@(Property ta ioa) b@(Property tb iob) = + Property (unionTargets ta tb) io + where + -- TODO pick with of ioa or iob to use based on final OS of + -- system being run on. + io = undefined + -- | The union of two lists of Targets. unionTargets :: Targeting l1 @@ -165,8 +183,12 @@ intersectTarget intersectTarget (Targeting l1) (Targeting l2) = Targeting $ nub $ filter (`elem` l2) l1 +-} + data CheckCombineTargets = CannotCombineTargets | CanCombineTargets +{- + -- | Detect intersection of two lists that don't have any common OS. -- -- The name of this was chosen to make type errors a more understandable. @@ -174,7 +196,9 @@ type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: type instance CannotCombineTargets l1 l2 '[] = 'CannotCombineTargets type instance CannotCombineTargets l1 l2 (a ': rest) = 'CanCombineTargets --- | Everything in the subset must be in the superset. +-} + +-- | Every target in the subset must be in the superset. -- -- The name of this was chosen to make type errors a more understandable. type family NotSupersetTargets (superset :: [a]) (subset :: [a]) :: CheckCombineTargets @@ -184,6 +208,8 @@ type instance NotSupersetTargets superset (s ': rest) = (NotSupersetTargets superset rest) 'CannotCombineTargets +{- + -- | Type level intersection of lists of Targets type family IntersectTarget (list1 :: [a]) (list2 :: [a]) :: [a] type instance IntersectTarget '[] list2 = '[] @@ -224,6 +250,8 @@ type instance EqTarget OSFreeBSD OSBuntish = 'False -- EqTarget a a = True -- EqTarget a b = False +-} + -- | An equivilant to the following is in Data.Type.Bool in -- modern versions of ghc, but is included here to support ghc 7.6. type family If (cond :: Bool) (tru :: a) (fls :: a) :: a @@ -243,5 +271,3 @@ type family Not (a :: Bool) :: Bool type instance Not 'False = 'True type instance Not 'True = 'False - --} -- cgit v1.2.3