Предотвращение объединения типов

Учитывая эту оболочку вокруг целых чисел:

newtype MyProxy a = MyProxy Int

mkProxy :: Int -> MyProxy a
mkProxy a = MyProxy a

addProxy :: MyProxy a -> MyProxy a -> MyProxy  a
addProxy (MyProxy a1) (MyProxy a2) = MyProxy $ a1+a2

Я могу выполнить следующее:

a = mkProxy 1
b = mkProxy 2
c = addProxy a b

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

Монада ST использует типы ранга 2 для достижения аналогичного эффекта. Вероятно, я мог бы сделать что-то подобное, изменив тип addProxy. Но я специально не хочу этого делать. Я хочу как-то аннотировать переменную типа a, чтобы предотвратить ее унификацию при вызове addProxy.

Возможно ли это в Haskell? Есть ли причина, по которой такой вариант может быть опасен?

Редактировать:

Позвольте мне остановиться на частичном решении (требующем -XScopedTypeVariables). Я могу переписать код выше как:

c :: forall a1 a2. MyProxy a1
c = addProxy a b
    where
        a = mkProxy 1 :: MyProxy a1
        b = mkProxy 2 :: MyProxy a2

Это правильно вызывает ошибку типа c, потому что a1 и a2 не могут быть объединены. Но у этого есть два недостатка: a и b нельзя определить на верхнем уровне; и вы должны явно указать результирующий тип mkProxy.

Можно ли исправить эти недостатки?


types haskell unification
person Mike Izbicki    schedule 15.05.2014    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Нет, вы не можете, по крайней мере, не указывая что-то еще для mkProxy.

Монада ST работает следующим образом: требует, чтобы экранирующие вычисления генерировали что-то типа forall s. ST s a, что не позволяет s появиться свободным в a.

Однако в вашем случае вы выполняете два идентичных вычисления, поэтому создание разных типов для каждого из них может быть использовано для совершения злых действий. Например, если mkInt 1 при каждом вызове генерирует разные типы,

class Evil a b c | a, b -> c where
  foo :: a -> b -> c

let x = mkProxy 1 in foo x x

Будет отличаться от

 foo (mkProxy 1) (mkProxy 1)

и мы потеряли некоторые очень хорошие свойства в нашем коде.

Однако мы можем проделать дополнительную работу и сделать явным тот факт, что a и b не могут унифицировать

 {-# LANGUAGE DataKinds #-}

 data Nat = S Nat | Z
 data Proxy (n :: Nat) a = Proxy a

 based :: a -> Proxy Z a
 based = Proxy

 fresh :: Proxy n a -> a -> Proxy (S n) a
 fresh (Proxy _) a = Proxy a

Итак, теперь вам нужно сделать что-то вроде

a = based 1

b = fresh a 2
person Daniel Gratzer    schedule 15.05.2014
comment
Я понимаю, почему пример foo был бы плохим, если бы mkProxy возвращал разные значения (многие оптимизации становятся небезопасными), но я не понимаю, почему плохо, что они возвращают разные типы. Что становится небезопасным? - person Mike Izbicki; 15.05.2014
comment
@MikeIzbicki Мы нарушаем ссылочную прозрачность, поскольку мы можем доказать, что используем перекрывающиеся экземпляры + классы типов с несколькими параметрами, чтобы различать выражение с поднятыми значениями и его встраивание вручную. По сути, классы типов позволяют нам различать точно так же, как и возвращать разные значения. - person Daniel Gratzer; 15.05.2014

arrow_upward
0
arrow_downward

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

{-# LANGUAGE ExistentialQuantification #-}

newtype MyProxy a = MyProxy Int

data Exists f = forall a. Exists (f a)

mkProxy :: Int -> Exists MyProxy
mkProxy a = Exists (MyProxy a)

addProxy :: MyProxy a -> MyProxy a -> MyProxy a
addProxy (MyProxy a1) (MyProxy a2) = MyProxy $ a1+a2

test :: Exists MyProxy -> Exists MyProxy -> Exists MyProxy
test (Exists a) (Exists b) = Exists (addProxy a b)
person Tom Ellis    schedule 15.05.2014
comment
Я считаю, что это работает по существу так же, как трюк с монадой ST. Причина, по которой мне это не подходит, заключается в том, что я хочу использовать функцию addProxy напрямую без оболочки. - person Mike Izbicki; 16.05.2014