Почему не GeneralizedNewtypeDeriving Безопасный Haskell?

Из руководства GHC, раздел Safe Language:

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

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

Источник

1 ответ

Решение

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

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

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 совсем по-другому, и эта реализация была безопасной. Безопасная реализация будет более ограниченной и более сложной.

ОБНОВЛЕНИЕ: С достаточно новыми версиями GHC (все проблемы должны быть устранены с 7.8.1) GeneralizedNewtypeDeriving безопасно из-за новой системы ролей

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