Является ли это безопасным использованием unsafeCoerce?

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

Код, который у меня есть, выглядит примерно так:

data Token b = Token !Integer

identical :: Token a -> Token b -> Bool
identical (Token a) (Token b) = a == b

data F a = forall b. F (Token b) (a -> b)

retrieve :: Token b -> F a -> Maybe (a -> b)
retrieve t (F t' f) = if identical t t' then Just (unsafeCoerce f) else Nothing

Две дополнительные вещи, которые следует отметить, заключаются в том, что эти токены используются в монаде, который я использую, чтобы гарантировать, что предложение целых чисел для них уникально (т.е. я не делаю то же самое в два раза). Я также использую переменную forall quantified shadow type так же, как и ST monad, чтобы убедиться, что (при условии, что используются только те методы, которые я раскрываю в модуле), нет способа вернуть токен (или, по сути, даже F) из монады, не являясь ошибкой типа. Я также не выставляю конструктор токенов.

Я думаю, что, насколько я вижу, это должно быть безопасное использование unsafeCoerce, как я могу сказать (надеюсь) довольно высокую уверенность в том, что ценность, которую я принуждаю, на самом деле является именно тем типом, которым я являюсь принуждая его, но я могу ошибаться. Я также попытался использовать Data.Typeable, который работает хорошо, но на данный момент я пытаюсь это избежать ограничения Typeable, тем более, что gcast, похоже, делает что-то во многом похожее, и мне все равно нужны токены, чтобы различать разные Fs того же типа.

Большое спасибо за любую помощь/совет.

Ответ 1

Вы внедрили ограниченную форму динамического набора текста, в основном следуя стилю Data.Dynamic - а именно, оценивая (непрозрачное) значение с подтверждением его типа, Во время выполнения вы можете сделать небезопасное принуждение, основанное на доказательствах, которые вы отправили с данными.

fromDyn (Dynamic t v) def
  | typeOf def == t = unsafeCoerce v
  | otherwise       = def

Это канонический подход, имеющий долгую историю, возвращающийся к:

Мартин Абади, Лука Карделли, Бенджамин Пирс и Гордон Плоткин. Динамическое типирование в статически типизированном языке. ACM-транзакции на языках программирования и системах, 13 (2): 237-268, апрель 1991 года.

Безопасность подхода зависит от непригодности токенов типа runtime. В вашем случае любой может создать токен, который приравнивает два типа - вам нужно будет гарантировать сопоставление 1-1 от типов к токенам и убедиться, что злоумышленник не может создавать неправильные токены. В случае GHC мы доверяем экземплярам Typeable (и абстракции модуля).

Ответ 2

Это не безопасно само по себе:

oops :: F Bool
oops = F (Token 12) not

bad :: Token Int
bad = Token 12

*Token> maybe 3 ($ True) $ retrieve bad oops
1077477808

F a является экзистенциально квантованным типом, вы не знаете, какой тип b попал в него. Поскольку identical не заботится о параметрах типа Token, он не может проверить, имеет ли поставляемый b от retrieve первый аргумент какое-либо отношение к тому, что было в F a.

Будет ли ваша защита

Две дополнительные вещи, которые следует отметить, заключаются в том, что эти токены используются в монаде, который я использую, чтобы гарантировать, что предложение целых чисел для них уникально (т.е. я не делаю то же самое в два раза). Я также использую переменную forall quantified shadow type так же, как и ST monad, чтобы убедиться, что (при условии, что используются только те методы, которые я раскрываю в модуле), нет способа вернуть токен (или, по сути, даже F) из монады, не являясь ошибкой типа. Я также не выставляю конструктор токенов.

достаточно силен, чтобы сделать его безопасным на практике, я не могу сказать, не видя его. Если действительно невозможно создать Token вне вычислений, а значение Integer Token однозначно характеризует параметр типа, это было бы безопасно.