haskell - 定义了一个类型族(++)；有什么方法可以证明 (vs++ us) ~ '[] implies (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 ~ '[] 意味着单独的 vs 和 us 的事实证明了这一点x 和 y 必然是 '[]。

有没有办法用类型族来做到这一点，或者可以切换到使用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