Является ли концепция "чередованного гомоморфизма" реальной вещью?
Мне нужен следующий класс функций:
class InterleavedHomomorphic x where
interleaveHomomorphism :: (forall a . f a -> g a) -> x f -> x g
Очевидно, что имя, которое я придумал для него, ни в коем случае не является официальным термином для чего-либо, и приведенный выше класс типов не очень элегантен. Это концепция, которая имеет имя, или даже реализацию в какой-то библиотеке? Есть ли более разумный способ сделать это?
Цель этой функции заключается в том, чтобы у меня был некоторый контекст f
это комментирует некоторые данные (Foo
а также Bar
это просто случайные примеры структур данных ради этого вопроса):
data Foo f = One (f (Bar f)) | Product (f (Foo f)) (f (Foo f))
data Bar f = Zero | Succ (f (Bar f))
Я хотел бы преобразовать контекст данных полиморфным способом; зная только гомоморфизм между контекстами и не (не обязательно) заботясь о самих данных. Это будет сделано путем предоставления instance InterleavedHomomorphic Foo
а также instance InterleavedHomomorphic Bar
в приведенном выше примере.
3 ответа
Итак, предполагая f
а также g
являются правильными функторами, forall a. f a -> g a
это естественная трансформация. Мы могли бы сделать это немного красивее:
type f ~> g = forall a. f a -> g a
Подобные естественные преобразования позволят нам сформировать категорию функторов Хаскелла, так что у вас есть функтор из этой категории.
Следуя шагам обычных функторов Хаскеля, возможно, имеет смысл x
быть эндофунктором, отображающим Функторы на другие Функторы. Это похоже, но не идентично тому, что у вас есть:
class FFunctor x where
ffmap :: (f ~> g) -> (x f ~> x g)
Тем не менее, в вашем случае x f
а также x g
не являются функторами, а x f -> x g
это нормальная функция, а не естественная трансформация. Тем не менее, шаблон достаточно близок, чтобы быть интригующим.
Имея это в виду, кажется, что x
все еще является примером функтора, просто между двумя разными категориями. Он переходит из категории функторов в категорию x
с разными структурами. Каждый возможный x
, лайк Foo
образует категорию с такими объектами, как Foo []
а также Foo Maybe
и преобразования между ними (Foo [] -> Foo Maybe
). Ваш interleaveHomomorphism
функция "поднимает" естественные превращения в эти x-morphisms
, как fmap
"поднимает" нормально (a -> b
) функции в функции в образе функтора (f a -> f b
).
Так что да: ваш класс типов является функтором Functor
за исключением двух разных категорий. Я не знаю конкретного имени для него, в основном потому, что я не знаю конкретного имени для таких конструкций, как x
,
В целом, я даже не уверен, что конкретное имя имело бы смысл. На данный момент, нам, вероятно, хотелось бы иметь хороший класс типов функторов, который идет между любыми двумя категориями. Может быть что-то вроде:
class (Category catA, Category catB) => GFunctor f catA catB where
gfmap :: catA a b -> catB (f a) (f b)
Это, вероятно, уже существует где-то в библиотеке.
К сожалению, этот конкретный подход к определению различных функторов потребовал бы кучу дополнительного шума нового типа, так как (->)
это уже категория. На самом деле, заставить все типы правильно выстроиться в линию будет немного больно.
Так что, наверное, проще всего назвать это XFunctor
или что-то. Кроме того, только представьте, что игра слов!
РЕДАКТИРОВАТЬ: похоже categories
обеспечивает CFunctor
типа, как это, но немного умнее:
class (Category r, Category s) => CFunctor f r s | f r -> s, f s -> r where
cmap :: r a b -> s (f a) (f b)
Однако я не уверен, что даже это достаточно общее! Я думаю, что мы могли бы хотеть, чтобы это было более полиморфным по видам также.
Bar f
выглядит как свободная монада Free f ()
,
затем Foo
это do
с одним или двумя <-
, Может быть, продолжить оттуда...
Для чего это стоит, вы можете перефразировать упрощенную версию вашего примера как
data Bar' r = Zero | Succ r
type Bar f = fix (Bar' . f)
Для каждой пары естественных преобразований eta1 :: f ~> g
а также eta2 :: Bar' ~> h
мы получаем естественную трансформацию (eta2 . eta1) :: (Bar' . f) ~> (h . g)
, И мы можем поднять это естественное преобразование над фиксированной точкой очевидным способом, чтобы получить fixed (eta2 . eta1) :: Bar f -> fix (h . g)
, Таким образом, ваш "чередующийся гомоморфизм" является лишь частным случаем этой конструкции, когда мы имеем eta2 = id
,
В целом это довольно стандартная конструкция (особенно для случаев, когда f
это монада или comonad), хотя я не уверен, что у него есть конкретное имя, которое широко признано.