CODEWITHSUNDEEP
haskell
user512596
user512596

Reputation:

how to write an intersection function for type-level lists

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

Upvotes: 4

Views: 133

Answers (1)

user512596
user512596

Reputation:

The main fix is as follows:

- type family ElemOSList a (list :: [b]) :: Bool
+ type family ElemOSList (a :: SupportedOS) (list :: [SupportedOS]) :: Bool

Also as noted there was a wrong base case.

Here's the fixed up code:

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

type family ElemOSList (a :: SupportedOS) (list :: [SupportedOS]) :: Bool
type instance ElemOSList a '[] = False
type instance ElemOSList a (b ': bs) = a == b || ElemOSList a bs

Upvotes: 2

Related Questions