代码之家 › 专栏 › 技术社区 › Justin L.

定义了类型族(++);有什么方法可以证明(vs++us)~'[]暗示(vs~'[])和(us~'[])?

type-families functional-dependencies haskell

3

Justin L. · 技术社区 · 10 年前

定义:

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(x) 和 y 是必然的 '[] .

是否有任何方法可以使用类型族来实现这一点,或者可以使用fundeps切换到多参数类型类方法?

谢谢

2 回复 | 直到 10 年前

1

6

effectfully 10 年前

Don't touch the green smile!

返回类型中存在绿色粘液定义的函数是一个危险的信号。

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

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

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

2

4

mniip 10 年前

您可以添加两个类型族,作为 ++ ,并且不失一般性地将它们作为约束添加到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