Полиморфная функция по экзистенциальному типу

Благодаря экзистенциальной квантификации я могу вызывать методы C для сигналов, но сигналы не выставляют параметр типа:

Теперь, поскольку C имеет ряд методов, моим естественным следующим шагом является вытащить функцию "уменьшить", чтобы я мог заменить любой метод:

Введите ошибку! Не удалось вывести (a1 ~ a). Дальнейшая мысль, я думаю, что это говорит о том, что 'f' является функцией в некотором экземпляре C, но я не могу гарантировать ему тот же экземпляр C, что и в Сигналах, потому что параметры типа скрыты! Я хотел этого, я понял.

Значит ли это, что невозможно обобщить reduceSig? Я могу жить с этим, но я настолько привык к тому, чтобы свободно разлагать функции в haskell, и странно, что он обязан писать шаблон. С другой стороны, я не могу придумать никакого способа выразить, что тип равен типу внутри Сигнала, не давая Сигналу параметр типа.

Ответы

Ответ 1

Что вам нужно выразить, так это то, что f, например reduce, используемый в reduceSig, может применяться к любому типу, который является экземпляром C, в отличие от текущего типа, где f работает на одном типе, который является экземпляром C. Это можно сделать так:

mapsig :: (forall a. (C a) => a -> a) -> Signal -> Signal
mapsig f (Signal sig) = Signal (map (second f) sig)

Вам понадобится расширение RankNTypes, как это часто бывает при использовании экзистенциальных типов; обратите внимание, что реализация mapsig одинаков, тип только что был обобщен.

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

Однако mapsig reduce не работает, по очевидной причине, что reduce :: (C a) => a -> Int, и вы не знаете, что a является Int! Вы должны дать mapsig более общий тип (с той же реализацией):

mapsig :: (C b) => (forall a. (C a) => a -> b) -> Signal -> Signal

т.е. f - это функция, принимающая любой тип, являющийся экземпляром C, и создающая тип, являющийся экземпляром C (этот тип фиксирован во время вызова mapsig и выбранный вызывающим устройством, т.е. когда значение mapsig f может быть вызвано на любом сигнале, оно всегда будет выдавать сигнал с тем же результатом (не то, что вы можете проверить это извне).

Экзистенциальные и ранговые типы N очень сложны, так что это может занять некоторое время, чтобы переварить.:)

Как добавление, стоит отметить, что если все функции из C выглядят как a -> r для некоторого r, тогда вам лучше создать запись, т.е. превратить

class C a where
  reduce :: a -> Int
  foo :: a -> (String, Double)
  bar :: a -> ByteString -> Magic

data Signal = forall a. (C a) => Signal [(Double, a)]

mapsig :: (C b) => (forall a. (C a) => a -> b) -> Signal -> Signal

data C = C
  { reduce :: Int
  , foo :: (String, Double)
  , bar :: ByteString -> Magic
  }

data Signal = Signal [(Double, C)]

mapsig :: (C -> C) -> Signal -> Signal

Эти два типа сигналов фактически эквивалентны! Преимущества прежнего решения появляются только тогда, когда у вас есть другие типы данных, которые используют C без экзистенциального количественного определения, так что вы можете использовать код, который использует специальные знания и операции конкретного экземпляра C, который он использует. Если ваши первичные варианты использования этого класса проходят через экзистенциальную количественную оценку, вы, вероятно, не хотите этого в первую очередь. Но я не знаю, как выглядит ваша программа:)