12

我的代码经常使用看起来像

foo :: (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

为了尝试缩短它，我编写了以下类型别名：

type FooT m a = (MyMonad m) => ListT m a

GHC 要求我打开 Rank2Types（或 RankNTypes），但当我使用别名将代码缩短为

foo :: MyType a -> MyOtherType a -> FooT m a

相比之下，当我写另一个类型别名时

type Bar a b = (Something a, SomethingElse b) => NotAsBar a b

并在负面位置使用它

bar :: Bar a b -> InsertTypeHere

GHC 大声斥责我错了。

我想我知道发生了什么，但我相信我可以从你的解释中得到更好的理解，所以我有两个问题：

  • 类型别名实际上在做什么/它们实际上是什么意思？
  • 有没有办法在这两种情况下都保持简洁？
4

2 回答 2

12

类型签名基本上包含三个部分：

  1. 变量声明（这些通常是隐式的）
  2. 变量约束
  3. 类型签名头

这三个元素本质上是叠加的。必须先声明类型变量，然后才能使用它们，无论是在约束中还是在其他地方，并且类约束作用于类型签名头中的所有用途。

我们可以重写您的foo类型，以便显式声明变量：

foo :: forall m a. (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

变量声明由forall关键字引入，并扩展到.. 如果你没有明确地引入它们，GHC 会自动将它们限定在声明的顶层。接下来是约束，直到=>. 剩下的就是类型签名头。

看看当我们尝试拼接您的type FooT定义时会发生什么：

foo :: forall m a. MyType a -> MyOtherType a -> ( (MyMonad m) => ListT m a )

类型变量m在 的顶层存在foo，但您的类型别名仅在最终值内添加约束！有两种方法可以修复它。您可以：

  • 将 forall 移到最后，所以m以后才存在
  • 或将类约束移到顶部

将约束移到顶部看起来像

foo :: forall m a. MyMonad m => MyType a -> MyOtherType a -> ListT m a

GHC 的启用建议是RankNTypes前者（有点，我仍然缺少一些东西），导致：

foo :: forall a. MyType a -> MyOtherType a -> ( forall m. (MyMonad m) => ListT m a )

这是有效的，因为m它没有出现在其他任何地方，而且它在箭头的右边，所以这两个意思本质上是一样的。

相比于bar

bar :: (forall a b. (Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

类型别名在负数位置时，更高级别的类型具有不同的含义。现在 to 的第一个参数bar必须是 and 中的多态，a并b具有适当的约束。这与通常的含义不同，bar调用者选择如何实例化这些类型变量。它不是

很可能，最好的方法是启用ConstraintKinds扩展，它允许您为约束创建类型别名。

type BarConstraint a b = (Something a, SomethingElse b)

bar :: BarConstraint a b => NotAsBar a b -> InsertTypeHere

它不像您希望的那样简洁，但比每次都写出长约束要好得多。

另一种方法是将您的类型别名更改为 GADT，但这会带来其他一些您可能不想引入的后果。如果您只是希望获得更简洁的代码，我认为这ConstraintKinds是最好的选择。

于 2013-01-29T15:18:51.710 回答
9

您可以将类型类约束本质上视为隐式参数 - 即认为

Foo a => b

作为

FooDict a -> b

whereFooDict a是类中定义的方法字典Foo。例如，EqDict将是以下记录：

data EqDict a = EqDict { equal :: a -> a -> Bool, notEqual :: a -> a -> Bool }

不同之处在于，每种类型的每个字典只能有一个值（对 MPTC 进行适当的概括），而 GHC 会为您填写其值。

考虑到这一点，我们可以返回您的签名。

type FooT m a = (MyMonad m) => ListT m a
foo :: MyType a -> MyOtherType a -> FooT m a

扩展到

foo :: MyType a -> MyOtherType a -> (MyMonad m => ListT m a)

使用字典解释

foo :: MyType a -> MyOtherType a -> MyMonadDict m -> ListT m a

这等效于将参数重新排序为

foo :: MyMonadDict m -> MyType a -> MyOtherType a -> ListT m a

这相当于字典变换的逆

foo :: (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

这就是你要找的。

但是，在您的另一个示例中，情况并非如此。

type Bar a b = (Something a, SomethingElse b) => NotAsBar a b
bar :: Bar a b -> InsertTypeHere

扩展到

bar :: ((Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

这些变量仍然在顶层量化（即

bar :: forall a b. ((Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

)，因为您在 的签名中明确提到了它们bar，但是当我们进行字典转换时

bar :: (SomethingDict a -> SomethingElseDict b -> NotAsBar a b) -> InsertTypeHere

我们可以看到这不等于

bar :: SomethingDict a -> SomethingElseDict b -> NotAsBar a b -> InsertTypeHere

这会产生你想要的。

很难想出一个现实的例子，其中类型类约束被用在与量化点不同的地方——我在实践中从未见过它——所以这里有一个不切实际的例子，只是为了证明正在发生的事情：

sillyEq :: forall a. ((Eq a => Bool) -> Bool) -> a -> a -> Bool
sillyEq f x y = f (x == y)

对比如果我们==在没有将参数传递给时使用 try 使用会发生什么f：

sillyEq' :: forall a. ((Eq a => Bool) -> Bool) -> a -> a -> Bool
sillyEq' f x y = f (x == y) || x == y

我们得到一个错误的No 实例。Eq a

(x == y)insillyEq得到它的Eqdict f; 它的字典形式是：

sillyEq :: forall a. ((EqDict a -> Bool) -> Bool) -> a -> a -> Bool
sillyEq f x y = f (\eqdict -> equal eqdict x y)

退后一步，我认为您在这里感到恐惧的方式会很痛苦-我认为您只想使用某些东西来量化其上下文，其中上下文被定义为“使用它的函数签名”。这个概念没有简单的语义。您应该能够将其Bar视为集合上的函数：它将两个集合作为参数并返回另一个集合。我不相信会有这样的功能供您尝试实现。

至于缩短上下文，您可以使用ConstraintKinds允许您制作约束同义词的扩展，因此至少您可以说：

type Bars a = (Something a, SomethingElse a)

要得到

bar :: Bars a => Bar a b -> InsertTypeHere

但是你想要的仍然是可能的——你的名字不足以让我说出。您可能想研究Existential Quantification和Universal Quantification，这是对类型变量进行抽象的两种方式。

故事的寓意：记住这=>就像->除了那些参数是由编译器自动填充的，并确保您尝试定义具有明确定义的数学含义的类型。

于 2013-01-29T22:19:37.790 回答