GeneralizedNewtypeDeriving

[migmit]

nponeccop обратил моё внимание на пример того, как расширения

> {-# LANGUAGE GADTs #-}

и

> {-# LANGUAGE GeneralizedNewtypeDeriving #-}

дают возможность сделать unsafeCoerce. Продублирую здесь, так как информация важная; оба расширения я использую достаточно часто, и мне не хотелось бы получить ошибку в рантайме.

> module UnsafeCoerce where

Итак, сооружаем тип, который засвидетельствует для нас, что два типа равны:

> data Same a b where Same :: Same a a

Ну, коль скоро они равны, один из них можно безопасно преобразовать в другой:

> coerce :: Same a b -> a -> b
> coerce Same a = a

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

> euclid :: Same a b -> Same a c -> Same b c
> euclid Same Same = Same

Пока всё хорошо.

Теперь заведём класс, принадлежность типа к которому означает, что этот тип — не что иное как ():

> class Unit a where unit :: Same () a

Ну и очевидный инстанс:

> instance Unit () where unit = Same

А вот теперь мы заведём новый тип, который будет притворяться ():

> newtype Tag a = Tag () deriving Unit

Фокус в том, что deriving Unit заставляет класс Unit солгать, что тип, дескать, и есть такой.

Ну, казалось бы, что в этом такого? Типы разные, но изоморфные, так что эта ложь кажется не такой уж ужасной. Однако, её можно развить:

> same :: Same (Tag a) (Tag b) -> Same a b
> same Same = Same

То есть, из того, что два (разных) типа равны, можно сделать вывод, что любые два типа равны.

Осталось только собрать всё это воедино:

> unsafeCoerce :: a -> a'
> unsafeCoerce = coerce $ same $ euclid unit unit

Вот. Всё это очень плохо. Получается, что мы мешаем две вещи: изоморфизм типов и их синтаксическое равенство. deriving Unit основывается на изоморфизме, а same Same = Same — на равенстве.

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

Update: в комментах помогли сформулировать, чем мне не нравится same Same = Same: даже если под табличками "яблоки" и "бананы" стоит одно и то же ведро говна, это не значит, что яблоки ничем не отличаются от бананов.