定义了一个类型族（++）；有什么方法可以证明 (vs ++ us) ~ '[] 意味着 (vs ~ '[]) 和 (us ~ '[])？

Question

定义：

type family (xs :: [*]) ++ (ys :: [*]) where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

我有一个 GADT 有点像

data Foo :: [*] -> * -> * where
  Foo0 :: a -> Foo '[] a
  Foo1 :: Foo '[a] a
  Foo2 :: Foo vs a -> Foo us a -> Foo (vs ++ us) a

我想做类似的事情

test :: Foo '[] Int -> Int
test (Foo0 x) = x
test (Foo2 x y) = test x + test y

但我不能在 x 或 y 上使用 test，因为必须证明 x ~ Foo '[] Int 和 y ~ Foo '[] Int。但是我想说，这是从vs ++ us ~ '[]表示x和y的个体vs和us必然是[=23]这一事实来证明的=].

有没有什么方法可以使用类型族来做到这一点，或者可以切换到使用 fundeps 的多参数类型类方法？

谢谢！

Answer 1

Don't touch the green smile!

The presence of ‘green slime’ — defined functions in the return types of constructors — is a danger sign.

最简单的解决方法是概括 test 然后实例化：

gtest :: Foo xs Int -> Int
gtest (Foo0 x) = x
gtest (Foo2 x y) = gtest x + gtest y

test :: Foo '[] Int -> Int
test = gtest

Answer 2

您可以添加两个类型族作为 ++ 的反函数，并且在不失一般性的情况下将它们添加为 Foo2 构造函数的约束。通过这些反类型族，GHC 将能够准确地推断出您的要求。

这是 CutX 和 CutY 的示例实现，使得 r ~ a ++ b <=> a ~ CutY r b <=> b ~ CutX r a.

type family (xs :: [*]) ++ (ys :: [*]) where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type family CutX (rs :: [*]) (xs :: [*]) where
    CutX '[] xs = '[]
    CutX rs '[] = rs
    CutX (r ': rs) (x ': xs) = CutX rs xs

type family ZipWithConst (xs :: [*]) (ys :: [*]) where
    ZipWithConst '[] ys = '[]
    ZipWithConst xs '[] = '[]
    ZipWithConst (x ': xs) (y ': ys) = y ': ZipWithConst xs ys

type CutY rs ys = ZipWithConst rs (CutX rs ys)

data Foo :: [*] -> * -> * where
  Foo0 :: a -> Foo '[] a
  Foo1 :: Foo '[a] a
  Foo2 :: (rs ~ (vs ++ us), us ~ CutX rs vs, vs ~ CutY rs us) => Foo vs a -> Foo us a -> Foo rs a

定义了一个类型族（++）；有什么方法可以证明 (vs ++ us) ~ '[] 意味着 (vs ~ '[]) 和 (us ~ '[])？

Defined a type family (++); any way to prove that (vs ++ us) ~ '[] implies (vs ~ '[]) and (us ~ '[])?

haskell

type-families

functional-dependencies