From 9e87165bd8d9b0c80e4efa5ebae22e913ecb18a1 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 8 Mar 2016 15:08:43 -0400 Subject: initial type-level OS list --- src/Propellor/Types/OS/Typelevel.hs | 92 +++++++++++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) create mode 100644 src/Propellor/Types/OS/Typelevel.hs (limited to 'src') diff --git a/src/Propellor/Types/OS/Typelevel.hs b/src/Propellor/Types/OS/Typelevel.hs new file mode 100644 index 00000000..70d82e43 --- /dev/null +++ b/src/Propellor/Types/OS/Typelevel.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-} + +module Propellor.Types.OS.TypeLevel ( + SupportedOS(..), + OSList(..), + debian, + buntish, + freeBSD, + unixlike, + combineSupportedOS, + intersectSupportedOS, +) where + +import Network.BSD (HostName) +import Data.Typeable +import Data.String +import Data.Type.Bool +import Data.Type.Equality + +-- | A supported operating system. +data SupportedOS = OSDebian | OSBuntish | OSFreeBSD + deriving (Show, Eq) + +-- | A type-level and value-level list of supported operating systems. +-- +-- If the list is empty, no operating system is supported. +data OSList (os :: [SupportedOS]) = OSList [SupportedOS] + deriving (Show, Eq) + +-- | Any unix-like OS. +unixlike :: OSList '[OSDebian, OSBuntish, OSFreeBSD] +unixlike = OSList [OSDebian, OSBuntish, OSFreeBSD] + +debian :: OSList '[OSDebian] +debian = typeOS OSDebian + +buntish :: OSList '[OSBuntish] +buntish = typeOS OSBuntish + +freeBSD :: OSList '[OSFreeBSD] +freeBSD = typeOS OSFreeBSD + +typeOS :: SupportedOS -> OSList os +typeOS o = OSList [o] + +-- FIXME, should type check +-- foo :: OSList '[OSDebian, OSFreeBSD] +-- foo = (debian `combineSupportedOS` freeBSD ) `intersectSupportedOS` unixlike + +-- | Combines two lists of supported OS's, yielding a list with the +-- contents of both. +combineSupportedOS + :: (r ~ ConcatOSList l1 l2) + => OSList l1 + -> OSList l2 + -> OSList r +combineSupportedOS (OSList l1) (OSList l2) = OSList (l1 ++ l2) + +-- | Type level concat for OSList. +type family ConcatOSList (list1 :: [a]) (list2 :: [a]) :: [a] +type instance ConcatOSList '[] list2 = list2 +type instance ConcatOSList (a ': rest) list2 = a ': ConcatOSList rest list2 + +-- | The intersection between two lists of supported OS's. +intersectSupportedOS + :: (r ~ IntersectOSList '[] l1 l2) + => OSList l1 + -> OSList l2 + -> OSList r +intersectSupportedOS (OSList l1) (OSList l2) = OSList (filter (`elem` l2) l1) + +-- | Type level intersection for OSList +type family IntersectOSList (coll :: [a]) (list1 :: [a]) (list2 :: [a]) :: [a] +type instance IntersectOSList coll '[] list2 = coll +type instance IntersectOSList coll (a ': rest) list2 = + If (ElemOSList a list2) + (IntersectOSList (a ': coll) rest list2) + (IntersectOSList coll rest list2) + +-- | Type level elem for OSList +type family ElemOSList a (list :: [b]) :: Bool +type instance ElemOSList a '[] = False +type instance ElemOSList a (b ': bs) = + If (a == b) + True + (ElemOSList a bs) + +-- | Type level equality for SupportedOS +type family EqOS (a :: SupportedOS) (b :: SupportedOS) where + EqOS a a = True + EqOS a b = False +type instance a == b = EqOS a b -- cgit v1.2.3