管理约束爆炸(Haskell)

Question

我正在编写一个函数,我想在Vectors上使用它.换句话说,我有类似的东西:

import qualified Data.Vector.Generic as G
foo :: (G.Vector v a, G.Vector v b, G.Vector v c, G.Vector v d) 
    => v a -> v b -> v c -> v d 

这样用户可以选择使用Unboxedvs StorableVectors等.

但是如果我需要将中间值放入其中v,我会得到Vector约束的组合爆炸,例如:

foo :: (G.Vector v a, G.Vector v b, G.Vector v c, G.Vector v d,
        G.Vector v (a, b), G.Vector v (a, c), G.Vector v (c, b))
    => v a -> v b -> v c -> v d 

我如何管理这种冗长？有没有办法要么

1)GHC隐式生成约束

2)以某种方式将约束重构为公共类

Answer 1

一个类型的家庭可以很方便:

{-# LANGUAGE TypeFamilies, KindSignatures, DataKinds, TypeOperators, ConstraintKinds #-}

import qualified Data.Vector.Generic as G
import GHC.Prim

type family Vectors v (a :: [*]) :: Constraint where
  Vectors v '[]       = ()
  Vectors v (a ': as) = (G.Vector v a, Vectors v as)

这将创建一个类型级别函数,该函数获取类型列表并对Vector具有这些类型的泛型s进行适当的约束.你可以像这样使用它:

foo :: (Vectors v [a, b, c, d, (a, b), (a, c), (c, b)]) => v a -> v b -> v c -> v d

这不是很理想,但它确实在一定程度上减少了代码.

处理元组约束的急剧增加

由于具有更多类型级别技巧的对类型,您可以更好地处理这种约束的爆炸:

type family Combinations v (a :: [*]) :: Constraint where
  Combinations v '[]       = ()
  Combinations v (a ': as) = (G.Vector v a, CombComponent v a as, Combinations v as)

type family CombComponent v (a :: *) (bs :: [*]) :: Constraint where
  CombComponent v a '[]       = ()
  CombComponent v a (b ': bs) = (G.Vector v (a, b), G.Vector v (b, a), CombComponent v a bs)

它有点复杂,但现在我们可以foo像这样编写第二个签名:

foo :: (Combinations v [a, b, c, d]) => v a -> v b -> v c -> v d

这也可以进一步推广,以允许签名,如:

foo :: (Combinations (G.Vector v) [a, b, c, d]) => v a -> v b -> v c -> v d