Я хотел бы объединить различные лифты в один класс
class Lift a b where
lift :: a -> b
, чтобы вместо fmap, liftA2, liftA3, * * 1003 можно было использовать lift *.
Теперь достаточно просто написать примеры для них:
instance Functor f => Lift (a -> b) (f a -> f b) where
lift = fmap
instance Applicative f => Lift (a -> b -> c) (f a -> f b -> f c) where
lift = liftA2
instance Applicative f => Lift (a -> b -> c -> d) (f a -> f b -> f c -> f d) where
lift = liftA3
Однако для liftA2 и выше имеется индуктивное свойство. То есть мы можем извлечь лифт из небольших лифтов. Например:
liftA2 f a b = (liftA f a) <*> b
liftA3 f a b c = (liftA2 f a b) <*> c
liftA4 f a b c d = (liftA3 f a b c) <*> d
liftA5 f a b c d e = (liftA4 f a b c d) <*> e
...
Поэтому я бы хотел вместо того, чтобы перечислять каждый лифт в качестве отдельного экземпляра, использовать индукцию для создания всех из них. Однако, хотя определение является индуктивным, у меня возникают проблемы с выражением взаимосвязи между одним подъемом и следующим алгебраически . То есть, хотя я могу описать это, это не комбинация lift s и простых комбинаторов.
Даже если я напишу их без разбора, мы увидим, что каждый уровень более сложный, чем последний:
liftA2 = ((<*>) .) . liftA
liftA3 = (((<*>) .) .) . liftA2
liftA4 = ((((<*>) .) .) .) . liftA3
liftA5 = (((((<*>) .) .) .) .) . liftA4
...
Теперь я думаю, что это можно обойти, добавив gh c natural к классу
class Lift (n :: Nat) (a :: Type) (b :: Type) | a b -> n where
lift :: a -> b
И затем используя вспомогательный класс типов для выполнения большого количества связующего Работа. Однако это решение было бы далеко не элегантным, и я рассматриваю его в основном как последнее средство, поскольку я бы предпочел не раздувать класс с Nat, используемым только для вычислений.
Есть ли способ, которым я индуктивно определяю lift без изменения определения класса, как это?