类型同义词的类限制？

Question

我想做类似的事情:(在伪代码中;这不会编译)

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

或者可能

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

但我不能这样做.

阅读后,我有一种感觉,要实现这一点,我需要RankNTypes扩展名或forall关键字,但我无法围绕这个...

有人可以帮忙吗？

编辑:我管理,而是"猜测语法":解决方案是,确实RankNTypes:

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

这有效,但RankNTypes扩展

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

同样有效.有什么区别,Num a =>看起来很自然的约束如何与n级类型相关？

所以问题仍然存在,但我正在寻找解释,而不是解决方案.

Answer 1

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

是一样的

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

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

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

在大多数情况下,类型同义词只是语法上的便利,因此每当您Vec在类型签名中看到时,您只需将括号括在其定义周围并替换:

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

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

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

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

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

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

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)

在上面的例子中,类约束没有引入更高的排名,因为约束被绑定到外部范围中的变量.但是,当我们在数据构造函数中使用同义词时,约束将变为隐式(存在)字典:

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写出来,但这似乎更像是一个实现工件而不是其他任何东西.我们可以争辩说语法可以用来向类型引入量词,这种证明了RankNType需求的合理性,但是我们同样可以说编译器应该检测是否有新的量词是合理的,并相应地进行(就像它的一样)已经完成了引入的存在...).