Подтвердить что ты не робот

Почему не GeneralizedNewtypeDeriving Safe Haskell?

Из руководства GHC, раздел Безопасный язык:

Управление границей модулей - код Haskell, скомпилированный с использованием безопасного языка, гарантирован только доступом к общедоступным символам, доступным через другие списки экспорта модулей. Важной частью этого является то, что безопасный скомпилированный код не может проверять или создавать данные с использованием конструкторов данных, которые он не может импортировать. Если модуль M устанавливает некоторые инварианты посредством тщательного использования его экспортного списка, то код, скомпилированный с использованием безопасного языка, который импортирует M, гарантированно соблюдает эти инварианты. Из-за этого Template Haskell и GeneralizedNewtypeDeriving отключены на безопасном языке, поскольку они могут использоваться для нарушения этого свойства.

Как можно разбить инварианты модуля с помощью GeneralizedNewtypeDeriving?

Ответ 1

Luqui связан с моим сообщением в блоге по этому вопросу. В принципе, GeneralizedNewtypeDeriving, как реализовано в GHC, предполагает, что определенный вид изоморфизма (а именно, функционально нерелевантный изоморфизм, подразумеваемый newtype) подразумевает равенство Лейбница. Это справедливо в Haskell 98, но это совсем не так для Haskell plus extensions.

То есть, newtype предоставляет пару функций

a -> b
b -> a

которые ничего не делают в ядре, но не удается заключить

forall f. f a -> f b

потому что f может быть функцией типа или GADT. Это форма равенства, необходимого для GeneralizedNewtypeDeriving

Даже в Haskell 98 он разбивает модульные границы. У вас могут быть такие вещи, как

class FromIntMap a where
  fromIntMap :: Map Int b -> Map a b

instance FromIntMap Int where
  fromIntMap = id

newtype WrapInt = WrapInt Int deriving FromIntMap

instance Ord WrapInt where
  WrapInt a <= WrapInt b = b <= a

который будет делать плохие вещи...

В моем блоге показано, как реализовать unsafeCoerce несколько способов с использованием других расширений (все безопасно) и GeneralizedNewtypeDeriving.. Я лучше понимаю, почему это сейчас, и гораздо увереннее, что GeneralizedNewtypeDeriving не может произвести unsafeCoerce без расширений стиля "System FC" (тип familes, GADT). Силл, это небезопасно, и его следует использовать с осторожностью, если вообще. Я понимаю, что Lennart Augustsson (пользователь augustss) реализовал его совсем по-другому в hbc, и эта реализация была безопасной. Безопасная реализация будет более ограниченной и более сложной.

UPDATE: с новыми версиями GHC (все проблемы должны быть удалены с 7.8.1) GeneralizedNewtypeDeriving является безопасным из-за новой = rel= "noreferrer" > role system