Гетерогенное эталонное равенство в Haskell - PullRequest
Новая
       16

Гетерогенное эталонное равенство в Haskell

4 голосов
/ 16 марта 2019

В GHC экземпляр равенства для IORef и STRef основан на следующей примитивной операции: 

sameMutVar# :: MutVar# s a -> MutVar# s a -> Int#

Я хотел бы иметь возможность вычислять гетерогенное равенство ссылок, 

sameReference :: IORef a -> IORef b -> Bool

(или аналогично для STRef с потенциально различными типами).Можно ли просто использовать unsafeCoerce для проверки равенства ссылок?Есть ли причина, по которой sameMutVar# не дана гетерогенная сигнатура типа?

РЕДАКТИРОВАТЬ: Чтобы добавить некоторый контекст, я хотел бы иметь это гетерогенное указание равенства, потому что я хочу использовать метод равенства, чтобы удалить конкретныйIORef a из списка IORef s, чьи типы количественно определены количественно.

1 Ответ

4 голосов
/ 19 марта 2019

Совершенно безопасно писать 

sameReference :: IORef a -> IORef b -> Bool
sameReference = unsafeCoerce ((==) :: IORef a -> IORef a -> Bool)

Было бы вполне разумно, если бы примопу был присвоен тип 

sameMutVar# :: MutVar# s a -> MutVar# s b -> Int#

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

То, что вы не можете сделать безопасно, - это заключить, что sameReference (r1 :: IORef a) (r2 :: IORef b) = True означает, что a и bтот же самый.Предположим, у вас было 

sameRefSameType :: IORef a -> IORef b -> Maybe (a :~: b)

Тогда вы могли бы легко написать 

oops :: Coercible a b => IORef a -> a :~: b
oops r = fromJust (sameRefSameType r (coerce r))

, предоставив поддельные доказательства того, что любые два принудительных типа равны.Вы должны быть в состоянии выяснить, как использовать GADT, чтобы добраться оттуда до mkUC :: IO (a -> b).

Я считаю , что было бы безопасно написать 

sameRefCoercibleTypes :: IORef a -> IORef b -> Maybe (Coercion a b)

Поскольку Даниэль Вагнер упомянул стабильные имена, я должен отметить, что ситуация для них еще хуже в этом контексте.Мне нужно начать с небольшого фона.Предположим, вы пишете 

f :: Either x Int -> Either x Bool
f (Left x) = Left x
f (Right _) = Right False

В первом случае было бы стыдно выделять свежий конструктор Left просто для изменения типа.Таким образом, GHC имеет низкоуровневую оптимизацию (после конвейера оптимизации от ядра к ядру), которая пытается превратить это в (по существу) 

f p@(Left x) = unsafeCoerce p
f (Right _) = Right False

Это означает, что вы можете иметь m :: Either x a и n :: Either x bгде m и n относятся к одному и тому же объекту кучи, несмотря на то, что a и b имеют совершенно не связанные типы.Если вы создадите стабильное имя для m и стабильное имя для n, то эти стабильные имена будут сравниваться одинаково!Если вы ставите хотя бы целых 

sameSNCoercibleTypes
  :: StableName a
  -> StableName b
  -> Maybe (Coercion a b)

, вы можете использовать m и n, чтобы «доказать» Coercible (Either x a) (Either x b), из которого вы можете конвертировать любой a в любой b.Это немного деликатно, но, поскольку это вообще возможно, предполагая, что в противном случае это небезопасно.

...