Преобразователи в Haskell и ограничение мономорфизма

Я реализовал преобразователи в Haskell следующим образом:

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (foldr)
import Data.Foldable

type Reducer b a = a -> b -> b
type Transducer a b = forall t. Reducer t b -> Reducer t a

class Foldable c => Collection c where
    insert :: a -> c a -> c a
    empty  :: c a

reduce :: Collection c => Transducer a b -> c a -> c b
reduce f = foldr (f insert) empty

mapping :: (a -> b) -> Transducer a b
mapping f g x = g (f x)

Теперь я хочу определить общую функцию map. Поэтому я загружаю приведенный выше код в GHCi:

Prelude> :load Transducer
[1 of 1] Compiling Main             ( Transducer.hs, interpreted )
Ok, modules loaded: Main.
*Main> let map = reduce . mapping

<interactive>:3:20:
    Couldn't match type ‘Reducer t0 b1 -> Reducer t0 a1’
                  with ‘forall t. Reducer t b -> Reducer t a’
    Expected type: (a1 -> b1) -> Transducer a b
      Actual type: (a1 -> b1) -> Reducer t0 b1 -> Reducer t0 a1
    Relevant bindings include
      map :: (a1 -> b1) -> c a -> c b (bound at <interactive>:3:5)
    In the second argument of ‘(.)’, namely ‘mapping’
    In the expression: reduce . mapping
*Main> let map f = reduce (mapping f)
*Main> :t map
map :: Collection c => (a -> b) -> c a -> c b

Поэтому я не могу определить map = reduce . mapping. Однако я могу определить map f = reduce (mapping f).

Я считаю, что эта проблема вызвана ограничением мономорфизма. Мне бы очень хотелось написать map = reduce . mapping вместо map f = reduce (mapping f). Отсюда у меня два вопроса:

  1. Что вызывает эту проблему? Действительно ли это ограничение мономорфизма?
  2. Как решить эту проблему?

haskell higher-rank-types transducer monomorphism-restriction
person Aadit M Shah    schedule 11.01.2015    source источник
comment
Это происходит из-за вывода типов с более высокими рангами. Ограничение мономорфизма здесь не имеет значения. Я полагаю, нет простого решения, кроме добавления аннотации типа или перехода к точечному определению.   -  person chi    schedule 11.01.2015
comment
Аннотации типов не помогают: let map :: Collection c => (a -> b) -> c a -> c b; map f = reduce (mapping f) по-прежнему выдает ту же ошибку.   -  person Aadit M Shah    schedule 11.01.2015
comment
Ошибка типа говорит вам, в чем именно заключается проблема. Тип mapping автоматически изменяется, чтобы переместить forall в левую часть (попробуйте :t mapping). Это допустимое (сохраняющее семантику) преобразование, но средство проверки типов ожидает правильный тип Transducer a b, а не Reducer t a -> Reducer t b (которые могут быть разными типами). Но когда вы пишете reduce (mapping f), программа проверки типов видит, что приложение mapping f должно иметь тип forall t. Reducer t b -> Reducer t a, который является правильным типом для аргумента reduce.   -  person user2407038    schedule 11.01.2015
comment
let map = ((.) :: (Transducer a b -> c a -> c b) -> ((a -> b) -> Transducer a b) -> (a -> b) -> (c a -> c b)) reduce mapping работает, но... фигня. Это (.), которому нужна аннотация.   -  person chi    schedule 11.01.2015
comment
Попробуйте data-fix, который дает вам более общий случай, чем датчики, называемые F-algebras. Преобразователи по существу представляют собой F-алгебры, но только для спискообразных структур.   -  person Heimdell    schedule 11.01.2015
comment
@chi, а нельзя ли это сделать, аннотируя тип каждого операнда? Все еще не весело, но уже не так уродливо.   -  person dfeuer    schedule 11.01.2015
comment
@dfeuer Нет, аннотирования операндов недостаточно. Проблема в том, что если вы пишете f (x :: forall a. ...), а f имеет полиморфный тип b -> ..., то b не преобразуется в forall a. ..., поскольку переменные типа могут быть созданы только во время вывода монотипов. Что происходит, так это то, что a получает новую константу skolem a0, а затем f больше не получает полностью полиморфное значение. (По крайней мере, это то, что я понял — я определенно не эксперт в том, как именно GHC делает вывод)   -  person chi    schedule 11.01.2015
comment
@dfeuer Гораздо более простое объяснение: если reduce объявлено как имеющее тип T, использование reduce :: T вместо просто reduce не сообщает GHC ничего, чего он еще не знает. Сигнатуры типов имеют значение, когда они сообщают GHC, как специализировать более общий тип: здесь reduce и mapping используются с их полной универсальностью, поэтому никакой специализации не требуется. Вместо этого (.) является специализированным.   -  person chi    schedule 11.01.2015
comment
Я столкнулся с вопросом с аналогичной проблемой и, надеюсь, смог объяснить, почему type там не работает лучше: stackoverflow.com/a/27944035/ 1308058   -  person phadej    schedule 14.01.2015

Ответы (1)


arrow_upward
5
arrow_downward

Если вы сделаете Transducer newtype, то GHC намного лучше проработает типы. Переменная экзистенциального типа не уйдет за пределы преобразователя области видимости и останется полиморфной.

Другими словами, с приведенным ниже определением map = reduce . mapping работает

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (foldr, map, (.), id)
import Control.Category
import Data.Foldable

type Reducer b a = a -> b -> b
newtype Transducer a b = MkTrans { unTrans :: forall t. Reducer t b -> Reducer t a }

class Foldable c => Collection c where
    insert :: a -> c a -> c a
    empty  :: c a

instance Collection [] where
  insert = (:)
  empty = []

reduce :: Collection c => Transducer a b -> c a -> c b
reduce f = foldr (unTrans f insert) empty

mapping :: (a -> b) -> Transducer a b
mapping f = MkTrans $ \g x -> g (f x)

filtering :: (a -> Bool) -> Transducer a a
filtering f = MkTrans $ \g x y -> if f x then g x y else y

map :: Collection c => (a -> b) -> c a -> c b
map = reduce . mapping

filter :: Collection c => (a -> Bool) -> c a -> c a
filter = reduce . filtering

instance Category Transducer where
  id = MkTrans id
  MkTrans f . MkTrans g = MkTrans $ \x -> g (f x)

dub :: Num a => a -> a
dub x = x + x

test1 :: [Int]
test1 = reduce (filtering even . mapping dub) [1..10]
-- [2,4,6,8,10,12,14,16,18,20]

test2 :: [Int]
test2 = reduce (mapping dub . filtering even) [1..10]
-- [4,8,12,16,20]

*Main> :t reduce . mapping
reduce . mapping :: Collection c => (a -> b) -> c a -> c b

Также вы можете проверить http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/, где определение — type Transducer a b =:: (a -> Constant (Endo x) a) -> (b -> Constant (Endo x) b), и другие. Также другие интересные обсуждения.

person phadej    schedule 12.01.2015
comment
Здесь кажется разумным сделать это newtype. Имейте в виду, однако, что многие замечательные вещи, которые вы можете сделать с lenses, зависят от открытого forall в простом type и не будут работать с новыми типами. Не уверен, насколько это может относиться и к преобразователям. - person leftaroundabout; 12.01.2015
comment
Составить преобразователи можно, сделав их Category. - person phadej; 12.01.2015
comment
Немного отредактировал ответ, добавил ссылку на ответ Reddit - person phadej; 12.01.2015
comment
возможно ли реализовать преобразователь taking аналогично mapping или filtering? Пытался сделать так - но не получилось :( Для меня самое сложное - повторно использовать taking, чтобы уменьшить n. - person d12frosted; 04.09.2015
comment
@d12frosted taking должен быть преобразователем с отслеживанием состояния. Чтобы соответствовать этим типам выше, должна быть возможность написать take n = foldr (taking n insert) empty для некоторых taking. Вскоре вы понимаете, что это невозможно. take является структурно индуктивным в n, а не в списке (как map или filter). Сделав newtype AutoReducer a b = a -> b -> (b, AutoReducer a b) можно было бы, но я не пробовал. - person phadej; 04.09.2015
comment
Я понимаю. Спасибо за ответ. Тогда я должен попробовать поиграть с AutoReducer. - person d12frosted; 06.09.2015