定义了一个类型族(++); 任何方式来证明(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

但我不能使用test的x或y因x ~ Foo '[] Int并y ~ Foo '[] Int必须证明.但我想说,这是一个事实证明,vs ++ us ~ '[]意味着个人vs和us的x和y必然'[].

有没有办法用类型系列做到这一点,或者可能切换到带有fundeps的多参数类型方法？

谢谢!

Answer 1

别碰绿色的笑容!

"绿泥" - 在构造函数的返回类型中定义的函数 - 的存在是一个危险的标志.

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

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

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