为什么Haskell不能在函数签名中推断数据类型的类型类？

Question

首先,这个问题并非100%特定于Haskell,请随意评论类型类,接口和类型的一般设计.

我正在阅读LYAH - 创建类型和类型类以下是我正在寻找更多信息的段落:

Data (Ord k) => Map k v = ...  

但是,在Haskell中,永远不要在数据声明中添加类型类约束.为什么？好吧,因为我们没有受益很多,但我们最终写了更多的类约束,即使我们不需要它们.如果我们将或者不将Ord k约束放在Map kv的数据声明中,我们将不得不将约束放入假定可以对地图中的键进行排序的函数中.但是如果我们不将约束放在数据声明中,我们就不必在函数的类型声明中放入(Ord k)=>,而不关心是否可以对键进行排序.这样一个函数的一个例子是toList,它只需要一个映射并将其转换为一个关联列表.它的类型签名是toList :: Map ka - > [(k,a)].如果Map kv在其数据声明中有一个类型约束,则toList的类型必须是toList ::(Ord k)=> Map ka - > [(k,a)],即使该函数不执行任何操作按顺序比较键.

首先,这似乎是合乎逻辑的 - 但是将类型类附加到类型上并没有好处吗？如果类型类型是类型的行为,那么为什么要通过使用类型(通过函数)来定义行为,而不是类型本身？我假设有一些元编程可以使用它,它肯定是很好的描述性代码文档.相反,这在其他语言中是一个好主意吗？指定对象应该在方法上遵循的接口是否理想,如果调用者不使用该方法,则对象不必符合接口？而且,为什么Haskell不能推断使用类型的函数Foo,必须引入类型Foo声明中标识的类型约束？是否有一个pragma来启用它？

我第一次看到它时,就会形成"这是一种黑客攻击(或解决方法)".在第二次阅读时有些想法,听起来很聪明.在第三次阅读时,对OO世界进行了一次计算,这听起来像是一次黑客攻击.

所以我在这里.

Answer 1

也许Map k v并不是说明这一点的最好例子.给定定义Map,即使有一些函数不需要(Ord k)约束,也没有可能的方法来构造Map没有它的东西.

人们经常会发现,即使您将约束视为原始设计的一个明显方面,类型也可以在没有特定约束的情况下使用函数子集.在这种情况下,将约束从类型声明中删除会使其更加灵活.

例如,Data.List包含大量需要的函数(Eq a),但是当然列表在没有该约束的情况下非常有用.

Answer 2

简短的回答是:Haskell这样做是因为这是语言规范的编写方式.

答案很长,需要引用GHC文档语言扩展部分:

可以使用GADT样式语法声明可以在标准Haskell-98语法中声明的任何数据类型.选择主要是风格,但GADT风格的声明在一个重要方面有所不同:它们对数据构造函数的类约束的处理方式不同.具体来说,如果构造函数被赋予类型类上下文,则通过模式匹配使该上下文可用.例如:

data Set a where
    MkSet :: Eq a => [a] -> Set a

(......)

所有这些行为都与Haskell 98对数据类型声明的上下文的特殊处理形成对比(Haskell 98报告的第4.2.1节).在Haskell 98中的定义

data Eq a => Set' a = MkSet' [a]

赋予MkSet'与上面的MkSet相同的类型.但是,不是提供(Eq a)约束,MkSet上的模式匹配'需要(Eq a)约束!GHC忠实地实现了这种行为,虽然它很奇怪.但对于GADT风格的声明,GHC的行为更有用,而且更直观.

Answer 3

在数据声明中避免类型类约束的主要原因是它们完全没有任何结果; 事实上,我认为GHC将这种类语境称为"愚蠢的语境".这样做的原因是类字典没有带有数据类型的值,因此您必须将它添加到对值进行操作的每个函数中.

作为一种"强制"操作数据类型的函数的类型类约束的方法,它也没有真正完成任何事情; 函数通常应该尽可能多态,那么为什么要将约束强加到不需要它的东西上呢？

此时,您可能认为应该可以更改ADT的语义,以便使用值来携带字典.事实上,这似乎是GADT的重点; 例如,你可以这样做:

data Foo a where { Foo :: (Eq a) => a -> Foo a }
eqfoo :: Foo t -> Foo t -> Bool
eqfoo (Foo a) (Foo b) = a == b

请注意,eqfoo的类型不需要Eq约束,因为它由Foo数据类型本身"携带".