如何編寫類型級別列表的交集函數

我正在編寫操作系統的類型級別列表，並且我編寫了兩個類型級別的函數，一個組合兩個列表，另一個組合兩個列表，另一個組合兩個列表。我無法讓相交功能正常工作。如何編寫類型級別列表的交集函數

（GHC 7.10.3）

這裏的組合功能，如預期工作：

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

這裏的路口功能，不大的工作：

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

我如何說服類型檢查器，這是很好的類型？

全碼：

{-# 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

來源

2016-03-08 Joey

嗯。 'IntersectOSList'[] list2 = list2'對我來說看起來像一個狡猾的基本案例。還有更多嗎？ – pigworker

我盯着這看不出什麼，但注意到ElemOSList的類型家族是錯誤的。第一個參數，特別是。 – Joey

是的，基本情況是錯誤的 – Joey

主要修復程序如下：

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

另外如所指出有錯誤的基礎案例。

這裏是搞掂代碼：

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

來源

2016-03-08 22:22:26 Joey

如何編寫類型級別列表的交集函數

回答

相關問題