是否可以使用类型类约束的类型同义词？ [英] Are type synonyms with typeclass constraints possible?

问题描述

所以，我正在写一个松散的程序，基于<一个href =http://www.cs.dartmouth.edu/~cs8/F2011/notes/11/Sudoku.lhs =noreferrer>这个，并且写了这个（因为它在原始）

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

没有什么特别的。
但是，我发现自己用这样的类型写了几个函数：

  Eq a =>第a行 - > ... 
  

所以我想也许我可以将这个约束写入类型同义词定义中，我的想法不应该那么复杂，对吧？如果编译器可以在函数中使用它，它应该作为一个类型的同义词工作。这里没有部分应用程序或任何东西或某种欺骗（对我来说）。

所以我试过这个：

  type Row a = Eq a => [a] 
  

这不起作用，编译器建议切换 RankNTypes 。该选项使它能够编译，但是这些函数仍然要求我在它们的类型声明中保留 Eq a => 。另外，如果我尝试像这样的类型同义词，就像之前那样键入Matrix a = [Row a] ，则会导致错误。

因此，我的问题是：

• 是否可以有一个类型同义词如果没有，为什么？




解决方案

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





这看起来有点荒谬：什么是（==）::等式a => a - > a - > a 然后？





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





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



 （==）:: forall a。公式a => a  - > a  - > 
（==）::∀a。公式a => a  - > a  - > 
（==）::Λa。 {方程a}  - > a  - > a  - > a 
  

这被称为系统F 。





请注意，这个签名中没有真正的约束，但是额外的参数： Eq - 类字典。




Feel free to change the title, I'm just not experienced enough to know what's really going on.

So, I was writing a program loosely based on this, and wrote this (as it is in the original)

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

Nothing special there. However, I found myself writing a couple of functions with a type like this:

Eq a => Row a -> ...

So I thought that perhaps I could write this constraint into the type synonym definition, because to my mind it shouldn't be that much more complicated, right? If the compiler can work with this in functions, it should work as a type synonym. There are no partial applications here or anything or some kind of trickery (to my eyes).

So I tried this:

type Row a = Eq a => [a]

This doesn't work, and the compiler suggested switching on RankNTypes. The option made it compile, but the functions still required that I leave the Eq a => in their type declarations. As an aside, if I tried also having a type synonym like type Matrix a = [Row a] like before, it results in an error.

So my question(s) are thus:

• Is it possible to have a type synonym with a typeclass constraint in its definition?

  • If not, why?

• Is the goal behind this question achievable in some other way?

解决方案

Constraints on a type variable can not be part of any Haskell type signature.

This may seem a bit of a ridiculous statement: "what's (==) :: Eq a => a -> a -> a then?"

The answer is that a doesn't really exist, in much the same way there is not really an x in the definition f x = x * log x. You've sure enough used the x symbol in defining that function, but really it was just a local tool used in the lambda-abstraction. There is absolutely no way to access this symbol from the outside, indeed it's not required that the compiler even generates anything corresponding to x in the machine code – it might just get optimised away.

Indeed, any polymorphic signature can basically be read as a lambda expression accepting a type variable; various writing styles:

(==) :: forall a . Eq a => a -> a -> a
(==) :: ∀ a . Eq a => a -> a -> a
(==) :: Λa. {Eq a} -> a -> a -> a

This is called System F.

Note that there is not really a "constraint" in this signature, but an extra argument: the Eq-class dictionary.

这篇关于是否可以使用类型类约束的类型同义词？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！