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: даже если под табличками "яблоки" и "бананы" стоит одно и то же ведро говна, это не значит, что яблоки ничем не отличаются от бананов.

Comments

[nponeccop.livejournal.com]

Ах ты ж! Я как-то пропустил мимо ушей, что GADTs тоже хватает.

Математическое замечание КО:

euclid - это аксиома транзитивности для отношений, в нашем случае отношений эквивалентности. И равенство, и изоморфизм транзитивны.

[migmit.livejournal.com]

Нет, это не транзитивность. Транзитивность была бы Same b a -> Same a c -> Same b c.

[nponeccop.livejournal.com]

Точно

[thinker8086.livejournal.com]

Эм, стоп.

А равенство что - не коммутативно?

[migmit.livejournal.com]

Коммутативно, а при чём тут?

[thinker8086.livejournal.com]

А тогда чем отличаются

> Same a b -> Same a c -> Same b c

и

> Same b a -> Same a c -> Same b c

?

[migmit.livejournal.com]

Порядком a и b в первом аргументе.

[qehgt.livejournal.com]

Пустое множество яблок оказалось тождественно пустому множеству бананов.

[migmit.livejournal.com]

Вместо () можно подставить что угодно.