Вопросы обобщающего функтора

Функтор в Control.Categorical. Функтор имеет следующее определение:

class (Category r, Category t) => Functor f r t | f r -> t, f t -> r where
  fmap :: r a b -> t (f a) (f b)

Но допустим, я хочу иметь функтор от обычных функций до стрелки Клейсли (возможно, это глупый пример) .

Я бы хотел такой тип:

fmap :: (Monad m) => (a -> b) -> Kleisli m a b

Ну, я могу позволить r = (->), t = Kleisli m получить:

fmap :: (Monad m) => (a -> b) -> Kleisli m (f a) (f b)

Но тогда что такое f?! Я действительно просто хочу, чтобы это исчезло. Я мог бы использовать Identity, разрешив f = Identity, но тогда я получаю:

fmap :: (Monad m) => (a -> b) -> Kleisli m (Identity a) (Identity b)

что потребует некоторой грязной распаковки.

Затем я подумал об определении Functor следующим образом:

class (Category r, Category t) => Functor r t where
  type family F r t x :: *
  fmap :: r a b -> t (F r t a) (F r t b)

Это позволяет мне определить экземпляр Functor для Kleisli следующим образом (без уродливой оболочки Identity):

instance (Monad m) => Functor (->) (Kleisli m) where
  type F (->) (Kleisli m) a = a
  fmap f = Kleisli (return . f)

И после этого я почти уверен, что я в:

fmap :: (Monad m) => (a -> b) -> Kleisli m a b

И это хорошо.

Теперь есть одна проблема, которую я могу сразу определить, а именно: для заданных параметров r и t для Functor исходное определение класса допускает несколько вариантов для f, тогда как с моим определением r и t определяют f. Это серьезная проблема, как бы я определяю сказать:

fmap :: (a -> b) -> (Maybe a -> Maybe b)

Я не могу тогда определить:

fmap :: (a -> b) -> ([a] -> [b])

Как и в обоих случаях, r = (->) и t = (->). Так что в настоящее время мой Functor даже не заменяет оригинальную версию Prelude.

Итак, теперь у меня есть несколько вопросов:

  1. Могу ли я изменить свое определение, чтобы r и t не определяли f (как в исходной версии)? Или для этого потребуются Injective Type Families (я с удовольствием скомпилирую голову в попробуйте, если это так).
  2. Могу ли я дополнительно изменить свое определение, чтобы f и r определяли t, а также f и t определяли r?
  3. После выполнения вышеуказанного (или нет, если это невозможно) каковы потенциальные последствия для вывода типа?
  4. Есть ли какие-либо другие плохие вещи в моем определении класса по сравнению с оригиналом, кроме таких вещей, как увеличение набора текста?
  5. Существуют ли какие-либо альтернативные подходы, которые по-прежнему позволяют мне определять функтор Клейсли без обертывания Identity, будучи «лучше» того, что я предложил (более полезная структура, лучший вывод типов и т. д.).

Мне жаль, что последние несколько вопросов немного расплывчаты, я понимаю, что вывод типа против общности часто является компромиссом, но я просто ищу некоторые мысли по этому поводу в этом конкретном случае.

(Этот вопрос частично следует из ответов на этот вопрос)


haskell functor category-theory
person Clinton    schedule 21.09.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Самое близкое, что вы могли бы получить, было бы

class (Category r, Category t) => Functor
          (f :: *) (r :: *->*->*) (t :: *->*->*) where
  type F f x :: *
  fmap :: Tagged f ( r a b -> t (F f a) (F f b) )

instance Functor [()] (->) (->) where
  type F [()] x = [x]
  fmap = Tagged map

instance (Monad m) => Functor (Kleisli m () ()) (->) (Kleisli m) where
  type F (Kleisli m () ()) x = x
  fmap = Tagged $ \f -> Kleisli $ return . f
person leftaroundabout    schedule 21.09.2015
comment
У меня возникло бы искушение использовать class .. => Functor (f :: k) ... с PolyKinds и удалить фиктивные вхождения () ниже. Хорошая это идея или нет, я не уверен на 100%. - person chi; 21.09.2015
comment
@chi Я думал написать это сам, но я не совсем согласен с PolyKinds. - person leftaroundabout; 21.09.2015