是否可以编写一个类型级函数,True如果一个类型级别列表包含另一个类型级别列表,则返回该函数？
这是我的尝试:
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module TypePlayground where
import Data.Type.Bool
type family InList (x :: *) (xs :: [*]) where
InList x '[] = 'False
InList x (x ': xs) = 'True
InList x (a ': xs) = InList x xs
type family ListContainsList (xs :: [*]) (ys :: [*]) where
ListContainsList xs (y ': ys) = InList y xs && ListContainsList xs ys
ListContainsList xs '[] = 'True
它适用于简单的情况:
data A
data B
data C
test1 :: (ListContainsList '[A, B, C] '[C, A] ~ 'True) => ()
test1 = ()
-- compiles.
test2 :: (ListContainsList '[A, B, C] '[B, C, A] ~ 'True) => ()
test2 = ()
-- compiles.
test3 :: (ListContainsList (A ': B ': '[C]) (B ': A ': '[C]) ~ 'True) => ()
test3 = ()
-- compiles.
test4 :: (ListContainsList '[A, C] '[B, C, A] ~ 'True) => ()
test4 = ()
-- Couldn't match type ‘'False’ with ‘'True’
但是这样的情况呢？
test5 :: (ListContainsList (A ': B ': a) a ~ 'True) => ()
test5 = ()
-- Should compile, but fails:
-- Could not deduce (ListContainsList (A : B : a0) a0 ~ 'True)
-- from the context (ListContainsList (A : B : a) a ~ 'True)
麻烦的是你已经通过对包含列表的结构的归纳来定义你的子集类型系列,但是你传递的是一个完全多态(未知)的列表,其结构对于GHC来说是一个谜.你可能认为GHC无论如何都能使用感应,但你错了.特别是,正如每种类型都有未定义的值一样,因此每种类型都有"卡住" 类型.一个值得注意的例子,GHC内部使用并通过(IIRC)出口GHC.Exts:
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family Any :: k
该Any类型的家庭是每个善良.所以你可以有一个类型级别列表Int ': Char ': Any,其中Any使用的是kind [*].但是,有没有办法来解构Any为':或[]; 它没有任何这种明智的形式.由于Any存在类型族,GHC无法按照您希望的方式安全地使用归纳.
如果你想让归纳在类型列表上正常工作,你真的需要像Benjamin Hodgson所说的那样使用单身或类似的东西.您不需要仅传递类型级别列表,还需要传递GADT,以证明类型级别列表已正确构造.递归破坏GADT在类型级列表上执行归纳.
类型级自然数具有相同的种类限制.
data Nat = Z | S Nat
type family (x :: Nat) :+ (y :: Nat) :: Nat where
'Z :+ y = y
('S x) :+ y = 'S (x :+ y)
data Natty (n :: Nat) where
Zy :: Natty 'Z
Sy :: Natty n -> Natty ('S n)
你可能希望证明
associative :: p1 x -> p2 y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))
但你不能,因为这需要感应x和y.但是,你可以证明
associative :: Natty x -> Natty y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))
没有麻烦.
对于Haskell社区特有的布尔类型家族似乎有一种痴迷.不要使用它们!在使用这种测试的结果时,你为自己做的工作比必要的多.
子集是一个可以用信息丰富的证据证明的命题.这是设计此类证据的一种简单方法.首先,可以在列表中找到元素的证明类型:
data Elem xs x where
Here :: Elem (x ': xs) x
There :: Elem xs x -> Elem (y ': xs) x
Elem的结构类似于自然数(比较There (There Here)有S (S Z)),但更多的类型.要证明元素在列表中,您可以为其提供索引.
data All f xs where
Nil :: All f '[]
Cons :: f x -> All f xs -> All f (x ': xs)
All证明了给定谓词适用于列表的每个元素.它的结构是一系列的证明f.
现在,列表是另一个列表的子集的证明类型很容易使用这些机器写下来.
type IsSubset xs ys = All (Elem ys) xs
IsSubset表示为xs可以找到每个元素的证明列表ys.
您可以IsSubset通过破解类型类系统来自动验证值的搜索,但这是另一篇文章.