Как неразрешимые экземпляры могут фактически повесить компилятор?

К тому времени, когда я впервые прочитал серьезную критику-XUndecidableInstancesЯ уже полностью привык к этому, рассматривая это как простое снятие раздражающего ограничения, которое Haskell98 должен сделать компиляторами проще в реализации.

На самом деле я сталкивался с множеством приложений, в которых требовались неразрешимые экземпляры, но ни в одном из них они не вызывали проблем, связанных с неразрешимостью. Пример Люка проблематичен по совершенно другой причине

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

- ну, это будет явно перекрываться любым надлежащим 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 where y::y
instance C y => C y where y=z
z :: C y=>y; z=y
main = print (y :: Int)

Но циклы времени выполнения не являются чем-то необычным, вы можете легко кодировать их в Haskell98.

Я также пробовал разные, менее прямые петли, такие как

{-# 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)

Опять же, нет проблем во время компиляции.

Итак, что на самом деле нужно, чтобы повесить компилятор в разрешении неразрешимых экземпляров классов типов?

Источник

3 ответа

Решение

Я не думаю, что я когда-либо повесил компилятор. Я могу получить переполнение стека, изменив ваш первый пример. Кажется, что происходит некоторое кэширование, поэтому нам нужно требовать бесконечную последовательность уникальных ограничений, например,

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 ())

что дает нам

• 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)

который говорит вам, как вы можете заставить его висеть, если вы действительно этого хотите. Я предполагаю, что если вы можете заставить его зависать без этого, вы нашли ошибку.

Я хотел бы услышать от кого-то, кто работает на GHC.

Источник

Самый простой способ получить "переполнение стека сокращения" - это использовать семейства типов:

type family Loop where
  Loop = Loop

foo :: Loop
foo = True

Я не знаю прямого способа получить на самом деле циклическую компиляцию на текущем GHC. Я вспоминаю получение циклов пару раз с GHC 7.11, но я помню только один в воспроизводимых деталях:

data T where
    T :: forall (t :: T). T

Но это было исправлено с тех пор.

Источник

К моему удивлению, UndecidableInstances может на самом деле повесить определенные версии GHC. Вот несколько строк кода, которые сделали это для меня:

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
module Nested where

class Nested r ix where

type family Lower ix :: *

data LN

instance Nested LN (Lower ix) => Nested LN ix where

data L

instance Nested LN ix => Nested L ix where

При компиляции как часть библиотеки (не напрямую ghc main.hs) этот код бесконечно висит на GHC 8.2.1

Как уже упоминалось @luqui, это похоже на ошибку, поэтому об этом сообщается так: https://ghc.haskell.org/trac/ghc/ticket/14402

Редактировать: Это оказалось действительно ошибкой, которая уже была исправлена ​​в текущей версии разработки GHC.

Источник
Другие вопросы по тегам