类型同义词的类限制? [英] Class restriction for type synonyms?

问题描述

我想做类似的事情: (以伪代码；这不会编译)

I want to do something like: (In pseudocode; this does not compile)

type Num a => Vector2d = (a,a)

或可能

type Num a => Vector2d a = (a,a)

但是我不能这样做.

阅读后，我有种感觉，要实现此目的，我需要RankNTypes扩展名或forall关键字，但是我无法解决这个问题……

After reading up I have a feeling that to achieve this I need the RankNTypes extension or the forall keyword, but I just can't wrap my mind around this...

任何人都可以帮忙吗?

我设法做到了，而是通过猜测语法"来实现的: 解决方案的确是使用RankNTypes:

I managed, but rather by "guessing around syntax": The solution is, indeed with RankNTypes:

type Vec =  forall a. Num a => (a,a)

此方法有效，但扩展名为RankNTypes

This works, but with the RankNTypes extension

type Vec = Num a => (a,a)

同样有效.有什么区别?看起来很自然的Num a =>约束与等级 n 类型有什么关系?

works equally. What's the difference, and how does a Num a => constraint, which seems quite natural, relate to rank n types?

所以问题仍然悬而未决，但是我正在寻找一种解释，而不是解决方案.

So the question is still open, but I'm looking for an explanation, rather than a solution.

推荐答案

type Vec = forall a. Num a => (a, a)

与

type Vec = Num a => (a, a).

原因是，GHC在最顶层的类型变量范围内隐式引入了没有相应forall的每个类型变量，例如:

The reason is that every type variable without a corresponding forall is implicitly introduced by GHC at the topmost type variable scope, for example:

const :: a -> b -> a
const :: forall a b. a -> b -> a -- the same thing

在大多数情况下，类型同义词只是语法上的方便，因此，只要在类型签名中看到Vec，就可以在其定义周围加上括号并替换:

For the most part type synonyms are just syntactic convenience, so whenever you see Vec in a type signature, you can just put parentheses around its definition and substitute:

Vec -> Vec -> Integer
-- equals:
(forall a. Num a => (a, a)) -> (forall a. Num a => (a, a)) -> Integer

有一个奇怪的例外，您不能仅仅盲目地替换类型.如果您有这样的类型同义词:

There is one weird exception, where you can't just blindly substitute in the types. If you have a type synonym like this:

type Vec a = Num a => (a, a) 

然后，Num约束在替换后会浮动到最外层范围:

then the Num constraint floats out to the outermost scope after substitution:

vec = (100, 100) :: Vec Integer
-- vec has now type "(Integer, Integer)"

和同一类型变量的多个约束合并:

and multiple constraints on the same type variable merge:

addVec :: Vec a -> Vec a -> Vec a
addVec (a, b) (c, d) = (a + c, b + d)
-- addVec has now effectively type "Num a => (a, a) -> (a, a) -> (a, a)

在上述情况下，类约束未引入更高的排名，因为约束被绑定到外部作用域中的变量.但是，当我们在数据构造函数中使用同义词时，约束将变为隐式(现有)字典:

In the above cases the class constraint didn't introduce higher-rankedness, because the constraints were bound to variables in the outer scope. However, when we use the synonym inside data constructors, the constraint turns into an implicit (existential) dictionary:

type Foo a = Num a => a 
data Bar a = Bar (Foo a) -- equals "data Bar a = Bar (Num a => a)"
-- requires ExistentialQuantifiaction or GADTs to compile

-- and of course, any data constructor blocks the outwards floating of the constraint:
type Baz = a -> (Foo a, ()) -- requires ImpredicativeTypes.

因此，总而言之，类型同义词中的这些约束的行为相当不稳定.我们需要RankNTypes或Rank2Types来将它们写出来，但这似乎比其他任何东西都更像是一种实现工件.我们可以说 syntax 可以用于将量词引入类型，并且这种情况证明了RankNType要求的合理性，但是我们可以同等地说，编译器应该检测是否有新鲜的东西是合理的.量词与否，然后进行相应的处理(例如已经使用引入的存在物完成了操作...).

So, to summarize, the behaviour of these kinds of constraints in type synonyms is rather wobbly. We need RankNTypes or Rank2Types to write them out, but this seems to be more of an implementation artifact than anything else. We could argue that the syntax can be used to introduce quantifiers to types, and this sort of justifies the RankNType requirement, but we could equally say that it's reasonable that the compiler should detect whether there are fresh quantifiers or not, and proceed accordingly (like it's already being done with the introduced existentials...).

这篇关于类型同义词的类限制?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！