具有类型类约束的类型同义词是否可行？

Question

随意更改标题,我只是没有经验足以知道真正发生了什么.

所以,我是基于这个松散地编写一个程序,并写了这个(因为它在原文中)

type Row a    = [a]
type Matrix a = [Row a]

没什么特别的.但是,我发现自己编写了几个类似这样的函数:

Eq a => Row a -> ...

所以我想也许我可以将这个约束写入类型同义词定义中,因为在我看来它不应该那么复杂,对吧？如果编译器可以在函数中使用它,它应该作为类型同义词.这里没有部分申请,也没有任何或某种诡计(对我来说).

所以我尝试了这个:

type Row a = Eq a => [a]

这不起作用,编译器建议启用RankNTypes.该选项使其编译,但函数仍然需要我留下Eq a =>他们的类型声明.顺便说一句,如果我尝试使用type Matrix a = [Row a]类似之前的类型同义词,则会导致错误.

所以我的问题是这样的:

• 是否可以在其定义中使用类型类型同义词和类型类约束？

  • 如果没有,为什么？

• 这个问题背后的目标是否可以通过其他方式实现？

Answer 1

对类型变量的约束不能是任何 Haskell 类型签名的一部分。

\n\n

这似乎是一个有点荒谬的说法：“然后呢(==) :: Eq a => a -> a -> a？”

\n\n

答案是，a实际上并不存在，就像不存在真正的东西一样。x定义中实际上并不存在 an 一样f x = x * log x。您确实已经x在定义该函数时使用了该符号，但实际上它只是 lambda 抽象中使用的本地工具。绝对没有办法从外部访问这个符号，实际上，编译器甚至不需要生成与机器代码 \xe2\x80\x93 中对应的任何内容x，它可能会被优化掉。

\n\n

事实上，任何多态签名基本上都可以被解读为接受类型变量的 lambda 表达式；各种写作风格：

\n\n

(==) :: forall a . Eq a => a -> a -> a\n(==) :: \xe2\x88\x80 a . Eq a => a -> a -> a\n(==) :: \xce\x9ba. {Eq a} -> a -> a -> a\n

\n\n

这就是所谓的系统 F。

\n\n

请注意，此签名中并没有真正的“约束”，而是一个额外的参数：Eq -class 字典。

\n