使用类约束理解rank 2类别别名 [英] Understanding a rank 2 type alias with a class constraint

问题描述

我有一些经常使用看起来像

的函数。 MyType a - > MyOtherType a - > ListT ma

为了缩短这个，我写了下面的类型别名：

  type FooT ma =（MyMonad m）=> ListT ma 
  

GHC让我打开Rank2Types（或RankNTypes），但没有抱怨，当我使用别名缩短我的代码到

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

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

时，

  type Bar ab =（Something a，SomethingElse b）=> NotAsBar ab 
  

并将其用于负数位置

  bar :: Bar ab  - > InsertTypeHere 
  

GHC大声大叫我错了。

我想我对发生了什么有了一个概念，但是我确信我可以从你的解释中得到更好的把握，所以我有两个问题：

• 实际在做什么类型的别名/它们实际意味着什么？


• 在两种情况下都有办法获得简洁性吗？

解决方案

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


$ b

变量声明

这三个元素本质上是叠加的。类型变量必须在可以使用之前进行声明，无论是在约束条件还是在其他地方使用，并且类约束作用域涵盖类型签名头中的所有用途。

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

  foo :: forall嘛。 （MyMonad m）=> MyType a  - > MyOtherType a  - > ListT ma 
  

变量声明由 forall 关键字，并扩展到。。如果您没有明确地介绍它们，GHC将自动将它们限定在声明的顶层。紧接着是约束条件，直至 => 。

看看我们试图拼接你的类型的FooT 定义时会发生什么：

  foo :: forall m a。 MyType a  - > MyOtherType a  - > （（MyMonad m）=> ListT ma）
  

类型变量 m 在 foo 的顶层被引入，但是你的类型别名只在最终值内添加一个约束！有两种方法来修复它。您可以：

• 将所有内容移动到最后，所以 m 进入以后存在


• 或将类约束移动到顶端

将约束移至顶端看起来像

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

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

  foo :: forall a。 MyType a  - > MyOtherType a  - > （MyMonad m）=> ListT ma）
  

这是可行的，因为 m 不会出现在其他地方，而且它是箭头的右边，所以这两个意思基本上是一样的。

比较 bar

  bar ::（forall a b。（Something a， SomethingElse b）=> NotAsBar ab） - > InsertTypeHere 
  

在类型别名为负数的情况下，高级类型具有不同的含义。现在， bar 的第一个参数在 a 和 b bar s调用者选择如何实例化这些类型变量。它不是

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

 类型BarConstraint ab =（Something a，SomethingElse b）
 
 bar :: BarConstraint ab => NotAsBar a b  - > InsertTypeHere 
  

它不像您期望的那么简洁，但比写出每个长约束更好时间。

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

I have code that frequently uses functions that look like

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

To try to shorten this, I wrote the following type alias:

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

GHC asked me to turn on Rank2Types (or RankNTypes), but didn't complain when I used the alias to shorten my code to

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

By contrast, when I wrote another type alias

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

and used it in a negative position

bar :: Bar a b -> InsertTypeHere

GHC loudly yelled at me for being wrong.

I think I have an idea of what's going on, but I'm sure I could get a better grasp from your explanations, so I have two questions:

• What are the type aliases actually doing/what do they actually mean?
• Is there a way to get the terseness in both cases?

解决方案

There are essentially three parts to a type signature:

1. variable declarations (these are usually implicit)
2. variable constraints
3. the type signature head

These three elements essentially stack. Type variables must be declared before they can be used, either in constraints or elsewhere, and a class constraint scopes over all uses within the type signature head.

We can rewrite your foo type so the variables are explicitly declared:

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

The variable declarations are introduced by the forall keyword, and extend to the .. If you don't explicitly introduce them, GHC will automatically scope them at the top level of the declaration. Constraints come next, up to the =>. The rest is the type signature head.

Look at what happens when we try to splice in your type FooT definition:

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

The type variable m is brought into existence at the top level of foo, but your type alias adds a constraint only within the final value! There are two approaches to fixing it. You can either:

• move the forall to the end, so m comes into existence later
• or move the class constraint to the top

Moving the constraint to the top looks like

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

GHC's suggestion of enabling RankNTypes does the former (sort of, there's something I'm still missing), resulting in:

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

This works because m doesn't appear anywhere else, and it's right of the arrow, so these two mean essentially the same thing.

Compare to bar

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

With the type alias in a negative position, a higher-rank type has a different meaning. Now the first argument to bar must be polymorphic in a and b, with appropriate constraints. This is different from the usual meaning, where bars caller chooses how to instantiate those type variables. It's not

In all likelihood, the best approach is to enable the ConstraintKinds extension, which allows you to create type aliases for constraints.

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

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

It's not quite as terse as what you hoped for, but much better than writing out long constraints every time.

An alternative would be to change your type alias into a GADT, but that has several other consequences you may not want to bring in. If you're simply hoping to get more terse code, I think ConstraintKinds is the best option.

这篇关于使用类约束理解rank 2类别别名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！