用fundeps捆绑约束

Question

我有一个foo带有一连串限制的函数.当然这些约束必须出现在使用的函数的签名中foo,所以我要做的是将foo约束包装在类型同义词中FooCtx a b ... :: Constraint.举个例子,

foo :: (A a, B b, C c, ...) => a -> b -> c

bar :: (A a, B b, C c, ...) ...
bar = ... foo ...

会成为

type FooCtx a b c ... = (A a, B b, C c, ...)
foo :: (FooCtx a b c) => a -> b -> c
bar :: (FooCtx a b c) => ...

如果暴露了所有类型,这将非常有用.但是,我正在使用函数依赖项来生成约束列表中的某些类型,并且这些类型不会出现在签名中foo.例如:

class Bar a b | a -> b

foo (Bar a b, ...) => a -> a

GHC不接受type FooCtx a = (Bar a b)因为b不受LHS的约束.我也不能使用,type FooCtx a b = (Bar a b)因为b它不在签名的范围内foo.签名foo将是foo :: (FooCtx a ?) => a -> a.

一个不令人满意的解决方案是将其中一个约束放入foo签名中,FooCtx以将fundep类型放入范围:

class Bar a b | a -> b

type FooCtx a b = ...

foo (Bar a b, FooCtx a b) => a -> a

但这违背了对约束进行分组的目的:

在遇到这种情况之前,我假设Constraint同义词可以盲目地替换任意约束列表.我知道封装这样的约束的唯一另一种方法是使用类,但是它遇到了同样的问题:class (A a, B b, C c, ...) => FooCtx a b c在LHS上不能有任何隐藏类型.还有其他方法我可以完全收集所有这些约束吗？

Answer 1

您误解了类型变量的绑定方式.他们不是由牛头型(绑定a -> a在你的例子)基础上,充分披类型的隐式粘合剂(但(Bar a b) => a -> a).可以使用ExplicitForAllGHC语言扩展来明确此绑定.

在你的例子中,当你写一些像

foo :: (Bar a b) => a -> a

那么完整的sigma类型,明确的tyvar绑定拼写出来,如下(因为在隐式的情况下,所有来自phi类型的tyvars都绑定在这里)

foo :: forall a b. (Bar a b) => a -> a

这意味着以相同的方式使用约束别名没有问题:如果你有例如

type FooCtx a b = (Bar a b, Num a, Eq a)

那么以下是有效的类型签名:

foo' :: forall a b. (FooCtx a b) => a -> a

因此,以下速记也是有效的:

foo' :: (FooCtx a b) => a -> a