Общие преобразования типов в Haskell

Позвольте мне посмотреть, понимаю ли я, что вы здесь ищете. У вас есть тип AV a, описывающий вычисление, производящее что-то типа a, где структура этого вычисления может быть сохранена таким образом, что это позволяет проводить проверку. Вам нужен способ преобразовать произвольные функции в операции над AV, сохраняя структуру и не создавая особых случаев для каждой операции.

Обычно для подъема функций в какую-либо структуру используются Functor и Applicative. Однако простой способ сделать это включает в себя преобразование структуры и применение расширенной функции напрямую, без сохранения приложения функции как части структуры.

То, что вы хотите, гораздо более неудобно, и вот почему:

Допустим, у нас есть некоторая функция, которую мы хотим поднять, и два абстрактных значения соответствующего типа, к которым ее можно применить:

x :: AV A
x = ...

y :: AV B
y = ...

f :: A -> B -> C
f = ...

Предположим, существует функция liftAV2, которая делает то, что вы хотите. Мы ожидаем, что тип lift2 f будет AV A -> AV B -> AV C, точно так же, как liftA для Applicative.

Позже мы хотим проверить вычисление, произведенное с использованием lift2 f, восстановив значения f, x и y. Предположим, что сейчас мы просто хотим извлечь первый аргумент. Предположим, что существует функция extractArg1, которая делает это, так что extractArg1 (liftAV2 f x y) = x. Что такое тип extractArg1? Здесь, в контексте, мы знаем, что он должен иметь тип AV C -> AV A. Но какого типа он будет вообще? Что-то вроде AV c -> AV a? Это неправильно, потому что результатом является не просто любой тип a, это тип, который использовался для построения значения AV c. Предполагая, что значение, с которым мы работаем, было построено с использованием результата liftAV2 f, мы знаем, что рассматриваемый тип существует, но у нас нет способа найти его вообще.

Здесь мы вступаем в страну, что вполне уместно, экзистенциальных типов. Честное использование их, не меньше, а не просто неправильное использование их с классами типов, как это часто бывает.

Вероятно, вы сможете добиться того, к чему стремитесь, приложив некоторые усилия, но это уже слишком продвинутая область. Для начала вы захотите использовать GADT, хотя я думаю, что вы, возможно, уже делаете это. Кроме того, очень неуклюже работать с экзистенциальными типами, потому что вы ограничены знанием того, что они из себя представляют, только в ограниченном контексте.

В вашем конкретном случае может быть проще указать AV два параметра типа: один представляет окончательный тип вычисления, а другой представляет структуру вычисления, например:

data f :$ x = ...

data AV structure result where
    ...
    AVApply :: AV f (a -> b) -> AV x a -> AV (f :$ x) b

Затем для проверки вычислений вы можете посмотреть на первый тип, чтобы узнать, что у вас есть; для построения вычислений вы можете посмотреть на второй, чтобы убедиться, что типы совпадают. Функция оценки будет иметь тип, подобный AV t a -> a, отбрасывая структуру. Вы также можете «распаковать» вычисление, используя тип структуры, отбросив тип результата, если вам нужно разобрать структуру, чтобы, скажем, красиво распечатать ее.

Как мне нравится думать об этом, я бы использовал экземпляр Functor, когда хочу поговорить о некоторых «данных с небольшим дополнением» (в зависимости от того, что такое «немного больше», я мог бы фактически говорить о Applicative или Monad ).

С другой стороны, я использую экземпляр Arrow, чтобы говорить о «функциях с меньшим количеством функций»: стрелки позволяют вам определять вещи, которые могут быть составлены вместе так же, как и функции, но вы можете добавить дополнительную структуру или ограничения, чтобы запретить определенные конструкции. (например, стрелки без ArrowChoice или ArrowLoop).

Не совсем понятно, чего вы хотите добиться, но похоже, что вы на самом деле оборачиваете свои данные в конструкторы типа AV. В этом случае вы, вероятно, захотите сделать AV экземпляром Functor и добавить Functor экземпляров для (AV a, AV b) => AV (a, b) и аналогичным образом для AV, обернутых вокруг Either.