summaryrefslogtreecommitdiff
path: root/src/Propellor/Types/MetaTypes.hs
diff options
context:
space:
mode:
authorJoey Hess2016-03-28 05:53:38 -0400
committerJoey Hess2016-03-28 05:55:48 -0400
commita1655d24bbb1db9caccdf93eae8110d746389ae2 (patch)
tree66b6890d852c19daec2306920fecf9108e055273 /src/Propellor/Types/MetaTypes.hs
parentebf30061d8f8a251330070e69c2710fe4a8fd9da (diff)
type safe targets for properties
* Property types have been improved to indicate what systems they target. This prevents using eg, Property FreeBSD on a Debian system. Transition guide for this sweeping API change: - Change "host name & foo & bar" to "host name $ props & foo & bar" - Similarly, `propertyList` and `combineProperties` need `props` to be used to combine together properties; they no longer accept lists of properties. (If you have such a list, use `toProps`.) - And similarly, Chroot, Docker, and Systemd container need `props` to be used to combine together the properies used inside them. - The `os` property is removed. Instead use `osDebian`, `osBuntish`, or `osFreeBSD`. These tell the type checker the target OS of a host. - Change "Property NoInfo" to "Property UnixLike" - Change "Property HasInfo" to "Property (HasInfo + UnixLike)" - Change "RevertableProperty NoInfo" to "RevertableProperty UnixLike UnixLike" - Change "RevertableProperty HasInfo" to "RevertableProperty (HasInfo + UnixLike) UnixLike" - GHC needs {-# LANGUAGE TypeOperators #-} to use these fancy types. This is enabled by default for all modules in propellor.cabal. But if you are using propellor as a library, you may need to enable it manually. - If you know a property only works on a particular OS, like Debian or FreeBSD, use that instead of "UnixLike". For example: "Property Debian" - It's also possible make a property support a set of OS's, for example: "Property (Debian + FreeBSD)" - Removed `infoProperty` and `simpleProperty` constructors, instead use `property` to construct a Property. - Due to the polymorphic type returned by `property`, additional type signatures tend to be needed when using it. For example, this will fail to type check, because the type checker cannot guess what type you intend the intermediate property "go" to have: foo :: Property UnixLike foo = go `requires` bar where go = property "foo" (return NoChange) To fix, specify the type of go: go :: Property UnixLike - `ensureProperty` now needs to be passed a witness to the type of the property it's used in. change this: foo = property desc $ ... ensureProperty bar to this: foo = property' desc $ \w -> ... ensureProperty w bar - General purpose properties like cmdProperty have type "Property UnixLike". When using that to run a command only available on Debian, you can tighten the type to only the OS that your more specific property works on. For example: upgraded :: Property Debian upgraded = tightenTargets (cmdProperty "apt-get" ["upgrade"]) - Several utility functions have been renamed: getInfo to fromInfo propertyInfo to getInfo propertyDesc to getDesc propertyChildren to getChildren * The new `pickOS` property combinator can be used to combine different properties, supporting different OS's, into one Property that chooses which to use based on the Host's OS. * Re-enabled -O0 in propellor.cabal to reign in ghc's memory use handling these complex new types. * Added dependency on concurrent-output; removed embedded copy.
Diffstat (limited to 'src/Propellor/Types/MetaTypes.hs')
-rw-r--r--src/Propellor/Types/MetaTypes.hs213
1 files changed, 213 insertions, 0 deletions
diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
new file mode 100644
index 00000000..e064d76f
--- /dev/null
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -0,0 +1,213 @@
+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}
+
+module Propellor.Types.MetaTypes (
+ MetaType(..),
+ UnixLike,
+ Linux,
+ DebianLike,
+ Debian,
+ Buntish,
+ FreeBSD,
+ HasInfo,
+ MetaTypes,
+ type (+),
+ sing,
+ SingI,
+ IncludesInfo,
+ Targets,
+ NonTargets,
+ NotSuperset,
+ Combine,
+ CheckCombine(..),
+ CheckCombinable,
+ type (&&),
+ Not,
+ EqT,
+ Union,
+) where
+
+import Propellor.Types.Singletons
+import Propellor.Types.OS
+
+data MetaType
+ = Targeting TargetOS -- ^ A target OS of a Property
+ | WithInfo -- ^ Indicates that a Property has associated Info
+ deriving (Show, Eq, Ord)
+
+-- | Any unix-like system
+type UnixLike = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish, 'Targeting 'OSFreeBSD ]
+-- | Any linux system
+type Linux = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]
+-- | Debian and derivatives.
+type DebianLike = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]
+type Debian = MetaTypes '[ 'Targeting 'OSDebian ]
+type Buntish = MetaTypes '[ 'Targeting 'OSBuntish ]
+type FreeBSD = MetaTypes '[ 'Targeting 'OSFreeBSD ]
+
+-- | Used to indicate that a Property adds Info to the Host where it's used.
+type HasInfo = MetaTypes '[ 'WithInfo ]
+
+type family IncludesInfo t :: Bool
+type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l
+
+type MetaTypes = Sing
+
+-- This boilerplate 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 Sing (x :: MetaType) where
+ OSDebianS :: Sing ('Targeting 'OSDebian)
+ OSBuntishS :: Sing ('Targeting 'OSBuntish)
+ OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
+ WithInfoS :: Sing 'WithInfo
+instance SingI ('Targeting 'OSDebian) where sing = OSDebianS
+instance SingI ('Targeting 'OSBuntish) where sing = OSBuntishS
+instance SingI ('Targeting 'OSFreeBSD) where sing = OSFreeBSDS
+instance SingI 'WithInfo where sing = WithInfoS
+instance SingKind ('KProxy :: KProxy MetaType) where
+ type DemoteRep ('KProxy :: KProxy MetaType) = MetaType
+ fromSing OSDebianS = Targeting OSDebian
+ fromSing OSBuntishS = Targeting OSBuntish
+ fromSing OSFreeBSDS = Targeting OSFreeBSD
+ fromSing WithInfoS = WithInfo
+
+-- | Convenience type operator to combine two `MetaTypes` lists.
+--
+-- For example:
+--
+-- > HasInfo + Debian
+--
+-- Which is shorthand for this type:
+--
+-- > MetaTypes '[WithInfo, Targeting OSDebian]
+type family a + b :: ab
+type instance (MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)
+
+type family Concat (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Concat '[] bs = bs
+type instance Concat (a ': as) bs = a ': (Concat as bs)
+
+-- | Combine two MetaTypes lists, yielding a list
+-- that has targets present in both, and nontargets present in either.
+type family Combine (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Combine (list1 :: [a]) (list2 :: [a]) =
+ (Concat
+ (NonTargets list1 `Union` NonTargets list2)
+ (Targets list1 `Intersect` Targets list2)
+ )
+
+-- | Checks if two MetaTypes lists can be safely combined.
+--
+-- This should be used anywhere Combine is used, as an additional
+-- constraint. For example:
+--
+-- > foo :: (CheckCombinable x y ~ 'CanCombine) => x -> y -> Combine x y
+type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine
+-- As a special case, if either list is empty, let it be combined with the
+-- other. This relies on MetaTypes list always containing at least
+-- one target, so can only happen if there's already been a type error.
+-- This special case lets the type checker show only the original type
+-- error, and not an extra error due to a later CheckCombinable constraint.
+type instance CheckCombinable '[] list2 = 'CanCombine
+type instance CheckCombinable list1 '[] = 'CanCombine
+type instance CheckCombinable (l1 ': list1) (l2 ': list2) =
+ CheckCombinable' (Combine (l1 ': list1) (l2 ': list2))
+type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine
+type instance CheckCombinable' '[] = 'CannotCombineTargets
+type instance CheckCombinable' (a ': rest)
+ = If (IsTarget a)
+ 'CanCombine
+ (CheckCombinable' rest)
+
+data CheckCombine = CannotCombineTargets | CanCombine
+
+-- | Every item in the subset must be in the superset.
+--
+-- The name of this was chosen to make type errors more understandable.
+type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine
+type instance NotSuperset superset '[] = 'CanCombine
+type instance NotSuperset superset (s ': rest) =
+ If (Elem s superset)
+ (NotSuperset superset rest)
+ 'CannotCombineTargets
+
+type family IsTarget (a :: t) :: Bool
+type instance IsTarget ('Targeting a) = 'True
+type instance IsTarget 'WithInfo = 'False
+
+type family Targets (l :: [a]) :: [a]
+type instance Targets '[] = '[]
+type instance Targets (x ': xs) =
+ If (IsTarget x)
+ (x ': Targets xs)
+ (Targets xs)
+
+type family NonTargets (l :: [a]) :: [a]
+type instance NonTargets '[] = '[]
+type instance NonTargets (x ': xs) =
+ If (IsTarget x)
+ (NonTargets xs)
+ (x ': NonTargets xs)
+
+-- | Type level elem
+type family Elem (a :: t) (list :: [t]) :: Bool
+type instance Elem a '[] = 'False
+type instance Elem a (b ': bs) = EqT a b || Elem a bs
+
+-- | Type level union.
+type family Union (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Union '[] list2 = list2
+type instance Union (a ': rest) list2 =
+ If (Elem a list2 || Elem a rest)
+ (Union rest list2)
+ (a ': Union rest list2)
+
+-- | Type level intersection. Duplicate list items are eliminated.
+type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Intersect '[] list2 = '[]
+type instance Intersect (a ': rest) list2 =
+ If (Elem a list2 && Not (Elem a rest))
+ (a ': Intersect rest list2)
+ (Intersect rest list2)
+
+-- | Type level equality
+--
+-- This is a very clumsy implmentation, but it works back to ghc 7.6.
+type family EqT (a :: t) (b :: t) :: Bool
+type instance EqT ('Targeting a) ('Targeting b) = EqT a b
+type instance EqT 'WithInfo 'WithInfo = 'True
+type instance EqT 'WithInfo ('Targeting b) = 'False
+type instance EqT ('Targeting a) 'WithInfo = 'False
+type instance EqT 'OSDebian 'OSDebian = 'True
+type instance EqT 'OSBuntish 'OSBuntish = 'True
+type instance EqT 'OSFreeBSD 'OSFreeBSD = 'True
+type instance EqT 'OSDebian 'OSBuntish = 'False
+type instance EqT 'OSDebian 'OSFreeBSD = 'False
+type instance EqT 'OSBuntish 'OSDebian = 'False
+type instance EqT 'OSBuntish 'OSFreeBSD = 'False
+type instance EqT 'OSFreeBSD 'OSDebian = 'False
+type instance EqT 'OSFreeBSD 'OSBuntish = 'False
+-- More modern version if the combinatiorial explosion gets too bad later:
+--
+-- type family Eq (a :: MetaType) (b :: MetaType) where
+-- Eq a a = True
+-- Eq 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
+type instance If 'True tru fls = tru
+type instance If 'False tru fls = fls
+type family (a :: Bool) || (b :: Bool) :: Bool
+type instance 'False || 'False = 'False
+type instance 'True || 'True = 'True
+type instance 'True || 'False = 'True
+type instance 'False || 'True = 'True
+type family (a :: Bool) && (b :: Bool) :: Bool
+type instance 'False && 'False = 'False
+type instance 'True && 'True = 'True
+type instance 'True && 'False = 'False
+type instance 'False && 'True = 'False
+type family Not (a :: Bool) :: Bool
+type instance Not 'False = 'True
+type instance Not 'True = 'False
+