haskell - 将类型族约束约束为 "some pair"

Question

考虑以下，我想说“a 是一对”:

type family F t a :: Constraint
type instance F Int a = (a ~ (a1, a2))

这不起作用，因为 a1和 a2不在范围内，但有没有办法表达这一点？

当然，在函数签名中，我可以编写约束，如 (a ~ (a1, a2))即使 a1和 a2其他地方没有提到，但我需要把它放在一个实例函数签名中，这当然是由类决定的。和 a在这种情况下不是实例本身的参数，只是实例函数，很像 Functor只有f作为类参数，而不是 a和 b ，所以我不能向实例子句添加额外的约束。

Answer 1

是的!你可以这样做!

强大的，有点内置的版本

首先，有几个有用的类型家族:

type family Fst a where
  Fst (x,y) = x

type family Snd a where
  Snd (x,y) = y

现在你所追求的:

type IsPair a = a ~ (Fst a, Snd a)

这是一个测试:

type family Con a where
  Con (f x y) = f

test :: IsPair a => proxy a -> Con a :~: (,)
test _ = Refl

还有一个更简单的测试一个更强大的属性:

 test1 :: IsPair a => a -> Fst a
 test1 = fst

并且只是为了确保它在应该满足的时候得到满足:

data Dict c where
  Dict :: c => Dict c

test2 :: Dict (IsPair (a, b))
test2 = Dict

当然，您可以使用它来定义您的 F :

type family F t a
type instance F Int a = IsPair a

更简单，但功能更弱

type family Con a where
  Con (f x y) = f
type IsPair a = Con a ~ (,)

与第一种方法相比，这种方法的问题在于它实际上并没有让您获得 a ~ (Fst a, Snd a) 的光荣知识。 .所以它发表了一个声明，但你不能用它做很多事情。

一点概括

为什么只是配对？如果你折腾PolyKinds混合，你可以得到非常一般的:

type family Arg1 a where Arg1 (f x) = x
type family Arg2 a where Arg2 (f y x) = y
type family Arg3 a where Arg3 (f z y x) = z
type family Arg4 a where Arg4 (f w z y x) = w

type family IsF (f :: k) (a :: *) :: Constraint
type instance IsF f a = a ~ f (Arg1 a)
type instance IsF f a = a ~ f (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg3 a) (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg4 a) (Arg3 a) (Arg2 a) (Arg1 a)

您可以在没有 PolyKinds 的情况下执行此操作也是，但是你需要 IsF1 , IsF2 ， 等等。

有了这个，

type IsPair a = IsF (,) a
type IsMaybe a = IsF Maybe a
...

泛化测试(这个东西只适用于 GHC 7.10 或更高版本；在此之前 polykinds 太脆弱了)。

data Dict c where
  Dict :: c => Dict c

test1 :: Dict (IsF f (f a))
test1 = Dict

test2 :: Dict (IsF f (f a b))
test2 = Dict

test3 :: Dict (IsF f (f a b c))
test3 = Dict

test4 :: Dict (IsF f (f a b c d))
test4 = Dict