gpt4 book ai didi

haskell - 如何为类型级列表编写交集函数

转载 作者:行者123 更新时间:2023-12-01 03:34:42 30 4
gpt4 key购买 nike

我正在研究操作系统的类型级列表,我编写了两个类型级函数,一个用于组合两个列表,另一个用于获取它们的交集。我无法让交集功能正常工作。

(gc 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

最佳答案

主要修复如下:

- 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

关于haskell - 如何为类型级列表编写交集函数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/35878018/

30 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com