类型检查器允许非常错误的类型替换,程序仍然编译

Question

在尝试调试我的程序中的问题时(使用Gloss将2个具有相同半径的圆圈绘制成不同的大小),我偶然发现了一个奇怪的情况.在我处理对象的文件中,我有以下定义*:

type Coord = (Float,Float)
data Obj =  Player  { oPos :: Coord, oDims :: Coord }

在导入Objects.hs的主文件中,我有以下定义:

startPlayer :: Obj
startPlayer = Player (0,0) 10

发生这种情况是因为我为玩家添加和更改字段,并且忘记更新Player之后(其尺寸由单个数字确定以表示半径,但我将其更改为a startPlayer来表示(宽度,高度);如果我做的话玩家对象是一个非圆圈).

令人惊奇的是,上面的代码编译并运行,尽管第二个字段是错误的类型.

我首先想到的可能是我打开了不同版本的文件,但对编译程序中的任何文件的任何更改都会反映出来.

接下来我认为可能Coord由于某种原因没有被使用.注释会startPlayer产生编译器错误,甚至更奇怪的是,更改startPlayerin 10会导致适当的响应(更改起始大小startPlayer); 再次,尽管它是错误的类型.为了确保它正确读取数据定义,我在文件中插入了一个拼写错误,它给了我一个错误; 所以我正在查看正确的文件.

我试图粘贴2段以上的到自己的文件,并吐出预期误差的第二场Player中Player是不正确.

什么可能允许这种情况发生？您认为这是Haskell的类型检查器应该阻止的事情.

---

我应该注意到,我原来的问题的答案,即两个被认为是相同半径的圆被绘制成不同的大小,其中一个半径实际上是负的.

Answer 1

这可能编译的唯一方法是存在Num (Float,Float)实例.标准库不提供此功能,尽管您使用的某个库可能因某些疯狂的原因而添加它.尝试在ghci中加载项目并查看是否10 :: (Float,Float)有效,然后尝试:i Num找出实例的来源,然后对定义它的人大喊大叫.

附录:没有办法关闭实例.甚至没有办法不从模块中导出它们.如果这是可能的话,那将导致代码更加混乱.这里唯一真正的解决方案是不定义这样的实例.

Answer 2

Haskell的类型检查是合理的.问题是你正在使用的图书馆的作者做了些什么......不太合理.

简短的回答是:是的,10 :: (Float, Float)如果有实例则完全有效Num (Float, Float).从编译器或语言的角度来看,它没有"非常错误".它与我们对数字文字的作用的直觉不相符.因为你已经习惯了类型系统捕捉到你所犯的那种错误,所以你有理由感到惊讶和失望!

Num实例和fromInteger问题

你很惊讶编译器接受了10 :: Coord,即10 :: (Float, Float).假设数字文字10将被推断为具有"数字"类型是合理的.开箱即用,数字文本可以被解释为Int,Integer,Float,或Double.没有其他背景的数字元组似乎不像这四种类型的数字.我们不是在谈论Complex.

然而,幸运或不幸的是,Haskell是一种非常灵活的语言.该标准指定将整数文字10解释为fromInteger 10具有类型的整数文字Num a => a.因此10可以推断为任何Num为其编写实例的类型.我在另一个答案中更详细地解释了这一点.

因此,当您发布问题时,经验丰富的Haskeller立即发现,10 :: (Float, Float)要获得接受,必须有一个像Num a => Num (a, a)或的实例Num (Float, Float).这里没有这样的实例Prelude,因此必须在其他地方定义.使用时:i Num,您很快发现了它的来源:gloss包裹.

输入同义词和孤立实例

但等一下.你gloss在这个例子中没有使用任何类型; 为什么实例gloss会影响你？答案有两个步骤.

首先,使用关键字引入的类型同义词type不会创建新类型.在您的模块中,写作Coord只是简写(Float, Float).同样地Graphics.Gloss.Data.Point,Point意思是(Float, Float).换句话说,你Coord和你gloss的Point字面上是等价的.

因此,当gloss维护者选择编写时instance Num Point where ...,他们也使您的Coord类型成为Num.这相当于instance Num (Float, Float) where ...或instance Num Coord where ....

(默认情况下,Haskell不允许类型同义词成为类实例.gloss作者必须启用一对语言扩展,TypeSynonymInstances并FlexibleInstances编写实例.)

其次,因为它是一个这是令人惊讶的孤儿情况,即一个实例声明instance C A,其中既C与A其他模块中的定义.在这里它特别阴险,因为所涉及的每个部分,即Num,(,)并且Float,来自Prelude并且可能在任何地方都在范围内.

你的期望是Num在Prelude,定义和Float定义的Prelude,所以关于这三个方面如何工作的所有内容都在中定义Prelude.为什么导入完全不同的模块会改变什么？理想情况下它不会,但孤儿实例打破了直觉.

(请注意,GHC警告有关孤儿实例 - gloss专门覆盖该警告的作者.这应该引起一个红旗,并在文档中至少提示警告.)

类实例是全局的,无法隐藏

此外,类实例是全球:是及物动词从进口任何模块中定义的任何情况下你的模块做实例分辨率时,会在背景和提供给typechecker.这使得全局推理变得方便,因为我们可以(通常)假设类函数(+)对于给定类型总是相同的.但是,这也意味着地方决策具有全球影响; 定义一个类实例不可逆转地改变下游代码的上下文,无法掩盖或隐藏它在模块边界之后.

您无法使用导入列表来避免导入实例.同样,您无法避免从您定义的模块导出实例.

这是Haskell语言设计中一个有问题且讨论很多的领域.在这个reddit线程中有一个关于相关问题的引人入胜的讨论.例如,请参阅Edward Kmett关于允许对实例进行可见性控制的评论:"您基本上抛弃了我编写的几乎所有代码的正确性."

(顺便说一下,正如这个答案所示,你可以通过使用孤立实例在某些方面打破全局实例假设!)

该怎么做 - 为图书馆实施者

在实施之前要三思Num.你不能解决的fromInteger问题-不,定义fromInteger = error "not implemented"并没有变得更好.您的用户是否会感到困惑或惊讶 - 或者更糟糕的是,从未注意到 - 如果他们的整数文字被意外推断为具有您要实例化的类型？提供(*)和(+)批评 - 特别是如果你必须破解它？

考虑使用库中定义的替代算术运算符,如Conal Elliott vector-space(对于类型*)或Edward Kmett linear(对于类型类型* -> *).这就是我自己倾向于做的事情.

使用-Wall.不要实现孤立实例,也不要禁用孤立实例警告.

或者,遵循linear许多其他表现良好的库的主角,并在以.OrphanInstances或结尾的单独模块中提供孤立实例.Instances.并且不要从任何其他模块导入该模块.然后,用户可以根据需要明确导入孤儿.

如果您发现自己定义了孤儿,请考虑让上游维护者在可能和适当的情况下实施它们.我曾经经常编写孤立实例Show a => Show (Identity a),直到他们添加它为止transformers.我甚至可能已经提出过关于它的错误报告; 我不记得了.

该怎么做 - 为图书馆消费者

你没有很多选择.超出礼貌和建设性地 - 到图书馆维护者.指出他们这个问题.他们可能有一些特殊的理由来编写有问题的孤儿,或者他们可能没有意识到.

更广泛地说:要意识到这种可能性.这是Haskell为数不多的具有真正全球影响的领域之一; 您必须检查导入的每个模块以及这些模块导入的每个模块是否都不实现孤立实例.类型注释有时会提醒您注意问题,当然您可以:i在GHCi中使用来检查.

如果它足够重要,请定义自己的newtypes而不是type同义词.你可以肯定没有人会搞砸他们.

如果您经常遇到来自开源库的问题,您当然可以创建自己的库版本,但维护很快就会成为一个令人头痛的问题.