不可否认的实例如何实际挂起编译器？ [英] How can undecidable instances actually hang the compiler?

问题描述

在我第一次阅读严肃的对 -XUndecidableInstances ，我已经完全习惯了，认为它只是解除了一个恼人的限制Haskell98让编译器更容易实现

  class Group g其中
（％）:: g  - > g  - > g 
 ... 
实例数字g => Group g，其中
 ... 
  

- 嗯，这显然是重叠的由Group 实例，所以不可判定性是我们最担心的：这实际上是非确定性的！！

但足够公平的是，我一直保留不可判定的实例可能会挂住编译器在我脑海中。

从哪里来当我阅读 CodeGolf.SE上的这个挑战时，需要购买代码会无限地挂起编译器。那么，听起来像是一个不可判定实例的工作，对吗？

原来我无法让他们这样做。以下内容至少从GHC-7.10开始编译：

  { - ＃LANGUAGE FlexibleInstances，UndecidableInstances＃ - } 
 class C y 
 instance C y => C y 
 main = return（）
  

我甚至可以使用类方法，只会在运行时导致循环：

  { - ＃LANGUAGE FlexibleInstances，UndecidableInstances＃ - } 
 class C y其中y :: y 
实例C y => C y其中y = z 
 z :: C y => y; z = y 
 main = print（y :: Int）
  

不寻常的是，你可以很容易地在Haskell98中编写这些代码。

我也尝试了不同的直接循环，比如

<$ p
数据B x = B
class C y
实例C （A x）=> C（B x）
实例C（B x）=> C（A x）

再次，编译时没有问题。

所以，实际上需要将编译器挂起来解析不可判定的类型实例吗？

解决方案

我不认为我真的挂过编译器。我可以通过修改第一个例子来获得堆栈溢出。看起来有一些缓存正在进行，所以我们需要一个无限序列的唯一约束，例如

  data A x = A派生（显示）
 class C y其中get :: y 
实例（C（A（A a）））=> C（A a）其中
 get = A 
 
 main = print（get :: A（））
  

这给了我们

$ $ $ $ $ $ $ $ $ $减少了堆栈溢出; （A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（A（A（A（A（A（A（A（A （A（A（A（A（A（A（A（A（））））））））））））））））））））））））））））） ）））））））））））））））））））））））））））））））））））））））））））））））））） ）））））））））））））））））））））））））））））））））））））））））））））））））） ）））））））））））））））））））））））））））））））））））））））））））））））））） ）））））））））））））））））
使用-freduction-depth = 0禁用此检查
（您可以选择的任何上限可能用$ b $无法预料地失败b对GHC进行较小的更新，因此如果
确定类型检查应该终止，建议禁用该检查）

告诉你如果你真的想要如何让它挂起。我的猜测是，如果你能在没有这个的情况下让它挂起，你就会发现一个bug。

我很想听听GHC工作的人的消息。 p>

By the time I first read serious criticism on -XUndecidableInstances, I had already completely accustomed to it, seeing it as merely removal of an annoying restriction Haskell98 has to make compilers easier to implement.

In fact I've encountered plenty of applications where undecidable instances were needed, but none where they actually caused any problems related to undecidability. Luke's example is problematic for quite a different reason

class Group g where
  (%) :: g -> g -> g
  ...
instance Num g => Group g where
  ...

– well, this would clearly be overlapped by any proper Group instance, so undecidability is the least of our worries: this is actually undeterministic!

But fair enough, I since kept "undecidable instances can possibly hang the compiler" in the back of my head.

Whence it was procured when I read this challenge on CodeGolf.SE, asking for code that would infinitely hang the compiler. Well, sounds like a job for undecidable instances, right?

Turns out I can't get them to do it. The following compiles in no time, at least from GHC-7.10:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y
instance C y => C y
main = return ()

I can even use class methods, and they'll only cause a loop at runtime:

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C y where y::y
instance C y => C y where y=z
z :: C y=>y; z=y
main = print (y :: Int)

But runtime loops are nothing unusual, you can easily code these in Haskell98.

I also tried different, less direct loops such as

{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
data A x=A
data B x=B
class C y
instance C (A x) => C (B x)
instance C (B x) => C (A x)

Again, no problem at compile time.

So, what is actually needed to hang the compiler up in resolution of undecidable type class instances?

解决方案

I don't think I've ever actually hung the compiler. I can get it to stack overflow though by modifying your first example. It seems that there is some caching going on, so we need to demand an infinite sequence of unique constraints, e.g.

data A x = A deriving (Show)
class C y where get :: y
instance (C (A (A a))) => C (A a) where
    get = A

main = print (get :: A ())

which gives us

• Reduction stack overflow; size = 201
  When simplifying the following type:
    C (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A (A ())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  Use -freduction-depth=0 to disable this check
  (any upper bound you could choose might fail unpredictably with
   minor updates to GHC, so disabling the check is recommended if
   you're sure that type checking should terminate)

which tells you how you could get it to hang if you really wanted to. My guess is that if you can get it to hang without this you've found a bug.

I'd love to hear from somebody who works on GHC.

这篇关于不可否认的实例如何实际挂起编译器？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！