haskell - 检查一个类型级列表是否包含另一个

Question

是否可以编写返回 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)

Answer 1

问题是您已经通过对包含列表的结构进行归纳定义了子集类型族，但是您传入的是一个完全多态(未知)的列表，其结构对 GHC 来说是个谜。你可能认为 GHC 无论如何都能使用归纳法，但你错了。特别是，就像每种类型都有未定义的值一样，每种类型都有“卡住”类型。一个值得注意的例子，GHC 在内部使用并通过 (IIRC) GHC.Exts 导出:

{-# LANGUAGE TypeFamilies, PolyKinds #-}

type family Any :: k

Any类型的家庭是各种各样的。所以你可以有一个类型级列表 Int ': Char ': Any , 其中 Any用于实物 [*] .但是没有办法解构 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))

没有麻烦。