Это безопасное использование 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, точно так же, как и монада ST, чтобы убедиться, что (при условии, что используются только методы, которые я раскрываю в модуле) нет способа вернуть токен (или фактически даже F) из монады без ошибки типа. Я также не открываю конструктор токенов.

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

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


types haskell dynamic-typing
person Community    schedule 14.01.2013    source источник
comment
Это очень похоже на Data.Typeable, который использует unsafeCoerce под прикрытием для реализации cast.   -  person Nathan Howell    schedule 14.01.2013
comment
Это очень похоже на это - на самом деле, я сказал это во второй части последнего абзаца вопроса. Спасибо, в любом случае.   -  person    schedule 14.01.2013
comment
Если вы эффективно копируете cast, то использование unsafeCoerce безопасно, но вы теряете сгенерированные компилятором typeOf/TypeRep. Вы можете использовать TypeRep вместо Integer в своем токене.   -  person Nathan Howell    schedule 14.01.2013
comment
Ну, первоначальная причина заключалась в том, что мне также нужно различать два разных значения с одним и тем же типом, но тогда может также потребоваться использовать Typeable/TypeRep.   -  person    schedule 14.01.2013

Ответы (2)


arrow_upward
14
arrow_downward

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

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

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

Мартин Абади, Лука Карделли, Бенджамин Пирс и Гордон Плоткин. Динамическая типизация на языке со статической типизацией. ACM Transactions on Programming Languages ​​and Systems, 13(2):237–268, апрель 1991 г.

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

person Don Stewart    schedule 14.01.2013

arrow_upward
9
arrow_downward

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

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, точно так же, как и монада ST, чтобы убедиться, что (при условии, что используются только методы, которые я раскрываю в модуле) нет способа вернуть токен (или фактически даже F) из монады без ошибки типа. Я также не открываю конструктор токенов.

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

person Daniel Fischer    schedule 14.01.2013