Экзистенциальный тип в функции более высокого порядка

У меня есть функция, задачей которой является вычисление некоторого оптимального значения типа a для некоторой функции значения типа a -> v

type OptiF a v = (a -> v) -> a

Затем у меня есть контейнер, который хочет сохранить такую ​​функцию вместе с другой функцией, которая использует значения:

data Container a = forall v. (Ord v) => Cons (OptiF a v) (a -> Int)

Идея состоит в том, что тот, кто реализует функцию типа OptiF a v, не должен беспокоиться о деталях v, за исключением того, что это экземпляр Ord.

Итак, я написал функцию, которая принимает такую ​​функцию значения и контейнер. Используя OptiF a v, он должен вычислить оптимальное значение wrt val и вставить его в контейнер result:

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int
optimize val (Cons opti result) = result (opti val)

Пока все хорошо, но я не могу назвать optimize, потому что

callOptimize :: Int
callOptimize = optimize val cont
   where val = (*3)
         opti val' = if val' 1 > val' 0 then 100 else -100
         cont = Cons opti (*2)

не компилируется:

Could not deduce (v ~ Int)
from the context (Ord v)
  bound by a type expected by the context: Ord v => Int -> v
  at bla.hs:12:16-32
  `v' is a rigid type variable bound by
      a type expected by the context: Ord v => Int -> v at bla.hs:12:16
Expected type: Int
  Actual type: Int
Expected type: Int -> v
  Actual type: Int -> Int
In the first argument of `optimize', namely `val'
In the expression: optimize val cont

где строка 12: 16-32 равна optimize val cont.

Неужели я не понимаю экзистенциальных типов в этом случае? Является ли forall v в объявлении optimize означать, что optimize может ожидать от a -> v любого v, который он хочет? Или это означает, что optimize не может ничего ожидать от a -> v, за исключением того, что Ord v?

Я хочу, чтобы OptiF a v не был исправлен для любого v, потому что позже я хочу подключить некоторое a -> v. Единственное ограничение, которое я хотел бы наложить, - Ord v. Можно ли даже выразить что-то подобное с использованием экзистенциальных типов (или что-то еще)?

Мне удалось добиться этого с помощью дополнительного typeclass, который предоставляет функцию optimize с аналогичной сигнатурой OptiF a v, но для меня это выглядит намного уродливее, чем использование функций более высокого порядка.

Ответы

Ответ 1

Это то, что легко ошибиться.

То, что у вас есть в сигнатуре optimize, не является экзистенциальным, а универсальным.

... так как экзистенты в любом случае устарели, перепишите ваши данные в форму GADT, что делает точку более ясной, поскольку синтаксис по существу такой же, как и для полиморфных функций:

data Container a where
  (:/->) :: Ord v =>                       -- come on, you can't call this `Cons`!
     OptiF a v -> (a->Int) -> Container a

Обратите внимание, что ограничение Ord (что подразумевает, что здесь forall v...) стоит вне сигнатуры функции с параметрической переменной, т.е. v - это параметр, который мы можем диктовать извне, когда мы хотим построить a Container. Другими словами,

Для всех v в Ord существует конструктор (:/->) :: OptiF a v -> (a->Int) -> Container a

что и дает название "экзистенциальный тип". Опять же, это аналог обычной полиморфной функции.

С другой стороны, в сигнатуре

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int

у вас есть forall внутри самого подписи, что означает, что какой конкретный тип v может принять участие, будет определяться вызываемым пользователем, optimize, внутренне - все, что мы контролируем извне, это он находится в Ord. Ничего "экзистенциального" об этом, поэтому эта подпись не будет компилироваться только с помощью XExistentialQuantification или XGADTs:

<interactive>:37:26:
    Illegal symbol '.' in type
    Perhaps you intended -XRankNTypes or similar flag
    to enable explicit-forall syntax: forall <tvs>. <type>

val = (*3), очевидно, не соответствует (forall v. (Ord v) => a -> v), на самом деле требуется экземпляр Num, который не у всех Ord. Действительно, optimize не должен иметь тип rank2: он должен работать для любого Ord -type v, который может дать ему вызывающий.

optimize :: Ord v => (a -> v) -> Container a -> Int

и в этом случае ваша реализация больше не работает: поскольку (:/->) - действительно экзистенциальный конструктор, он должен содержать только любую функцию OptiF для неизвестного типа v1. Таким образом, вызывающий оптимизатор имеет свободу выбора opti-функции для любого конкретного типа и функцию, которая должна быть оптимизирована для любого возможного другого фиксированного типа - это не может работать!

Решение, которое вы хотите, следующее: Container не должно быть экзистенциальным! Оптическая функция должна работать для любого типа, который находится в Ord, а не только для одного конкретного типа. Ну, как GADT, это выглядит примерно так же, как и для универсальной квантовой подписи, которую вы первоначально использовали для optimize:

data Container a where
  (:/->) :: (forall v. Ord v => OptiF a v) -> (a->Int) -> Container a

С этим теперь оптимизируйте работу

optimize :: Ord v => (a -> v) -> Container a -> Int
optimize val (opti :/-> result) = result (opti val)

и может использоваться по вашему желанию

callOptimize :: Int
callOptimize = optimize val cont
   where val = (*3)
         opti val' = if val' 1 > val' 0 then 100 else -100
         cont = opti :/-> (*2)