полиморфная функция по экзистенциальному типу - PullRequest
Новая
       6

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

14 голосов
/ 17 декабря 2011

Скажем, у меня есть класс: 

class C a where
  reduce :: a -> Int

Теперь я хочу упаковать его в тип данных: 

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

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

reduceSig :: Signal -> [(Double, Int)]
reduceSig (Signal sig) = map (second reduce) sig

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

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

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

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

1 Ответ

18 голосов
/ 17 декабря 2011

Вы должны выразить, что 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 принимает решение, в какую a вызывается функция; с вашим предыдущим типом вызывающий из mapsig решает, что не работает, потому что только mapsig знает правильный a , то есть тот, который находится внутри 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 может быть вызвано для любого сигнала, в результате он всегда будет выдавать сигнал с одинаковым a (не то, что вы можете проверить это со стороны).)

Экзистенциалы и типы ранга 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 он использует. Если ваши основные сценарии использования этого класса выполняются посредством экзистенциальной количественной оценки, вы, вероятно, не хотите этого в первую очередь. Но я не знаю, как выглядит ваша программа:)

...