how to write an intersection function for type-level lists

Viewed 123

I'm working on type-level lists of operating systems, and I wrote two type-level functions, one to combine two lists, and the other to take their intersection. I'm having trouble getting the intersection function to work right.

(ghc 7.10.3)

Here's the combine function, working as expected:

*Main> (combineSupportedOS debian freeBSD)  :: OSList '[OSDebian, OSFreeBSD]
OSList [OSDebian,OSFreeBSD]

Here's the intersection function, not quite working:

*Main> (intersectSupportedOS debian debian)  :: OSList '[OSDebian]
Couldn't match expected type ‘IntersectOSList ['OSDebian] '['OSDebian]’
            with actual type ‘'['OSDebian]’

How can I convince the type checker that this is well typed?

Full code:

{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-}

import Data.Typeable
import Data.String
import Data.Type.Bool
import Data.Type.Equality

data SupportedOS = OSDebian | OSFreeBSD
    deriving (Show, Eq)

data OSList (os :: [SupportedOS]) = OSList [SupportedOS]
    deriving (Show, Eq)

debian :: OSList '[OSDebian]
debian = typeOS OSDebian

freeBSD :: OSList '[OSFreeBSD]
freeBSD = typeOS OSFreeBSD

typeOS :: SupportedOS -> OSList os
typeOS o = OSList [o]

combineSupportedOS
    :: (r ~ ConcatOSList l1 l2)
    => OSList l1
    -> OSList l2
    -> OSList r
combineSupportedOS (OSList l1) (OSList l2) = OSList (l1 ++ l2)

type family ConcatOSList (list1 :: [a]) (list2 :: [a]) :: [a]
type instance ConcatOSList '[] list2 = list2
type instance ConcatOSList (a ': rest) list2 = a ': ConcatOSList rest list2

intersectSupportedOS
    :: (r ~ IntersectOSList l1 l2)
    => OSList l1
    -> OSList l2
    -> OSList r
intersectSupportedOS (OSList l1) (OSList l2) = OSList (filter (`elem` l2) l1)

type family IntersectOSList (list1 :: [a]) (list2 :: [a]) :: [a]
type instance IntersectOSList '[] list2 = list2
type instance IntersectOSList (a ': rest) list2 = 
    If (ElemOSList a list2)
        (a ': IntersectOSList rest list2)
        (IntersectOSList rest list2)

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 family EqOS (a :: SupportedOS) (b :: SupportedOS) where
    EqOS a a = True
    EqOS a b = False
type instance a == b = EqOS a b
1 Answers
Related