了解具有类约束的rank 2类型别名

Question

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

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大声喊叫我错了.

我想我已经知道发生了什么,但我相信我能从你的解释中更好地掌握,所以我有两个问题:

• 实际上做什么类型的别名/它们实际意味着什么？
• 有没有办法在这两种情况下获得简洁？

Answer 1

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

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

如果类型别名处于否定位置,则较高等级类型具有不同的含义.现在第一个参数bar必须是多态的,a并且b有适当的约束.这与通常的含义不同,其中bars调用者选择如何实例化那些类型变量.不是

在所有可能性中,最好的方法是启用ConstraintKinds扩展,这允许您为约束创建类型别名.

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

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

它并不像你希望的那样简洁,但比每次写出长约束要好得多.

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

Answer 2

您可以将类型类约束视为隐式参数 - 即考虑

Foo a => b

如

FooDict a -> b

where FooDict 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

我们得到一个没有Eq a错误的实例.

将(x == y)在sillyEq得到它的Eq字典从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

但你想要的仍然是可能的 - 你的名字对我来说不够描述.您可能希望研究存在量化和通用量化,这是抽象类型变量的两种方式.

这个故事的寓意:请记住,=>就像->除了这些参数是由编译器自动填入,并确保你正在试图定义类型的定义明确的数学含义.