Сумма индексированных функторов

Question

В Slicing It Conor McBride разрабатывает индексированные функторы, а затем описывает их суммы и продукты на слайде «Сумма и продукт» (слайды не маркированы, около 90% в презентации). Этот слайд начинается

-- sum - choose between compatible structures 
data (:+:) :: (i ->- o) -> (i ->- o) -> (i ->- o) where 
    L :: s x :-> (s :+: t) x 
    R :: t x :-> (s :+: t) x 
instance (IFunctor s, IFunctor t) => IFunctor (s :+: t) where 
    imap f (L sx) = L (imap f sx) 
    imap f (R tx) = R (imap f tx) 

В частности, это определение :+: требует, чтобы оба индексированных функторов имеют одинаковый индекс источника i. Интересно, почему это так. Можно ли это смягчить, например? к позволяя

-- sum - choose between compatible structures 
data (:+:) :: (i ->- o) -> (j ->- o) -> (Either i j ->- o) where 
    L :: s x :-> (s :+: t) x 
    R :: t x :-> (s :+: t) x 

где i и j являются в настоящее время различные типы?

Answer 1

@chi Спасибо за указатель. Оказывается, я ошибался - мое предложение не работает, невозможно комбинировать разные входы. Тем не менее, можно использовать Either для выходных видов, что приводит к конструктору @chi предложил:

data (:+:) :: (i ->- o) -> (i ->- u) -> (i ->- Either o u) where 
    L :: s x o -> (s :+: t) x ('Left o) 
    R :: t x u -> (s :+: t) x ('Right u) 

И :+: и :*: типов на слайдах принимают два типа в качестве аргументов, то есть по существу пара аргументов , Я считаю, что мое предложение могло бы работать, если они приняли альтернативу (т.е. Either) аргументов типа, как и в

data (:|:) :: Either (i ->- o) (j ->- o) -> (Either i j ->- o)