Как я могу объединить два типа ограничений с логическим или в Haskell?

В Haskell нам предоставляется возможность комбинировать ограничения для типов с логическим и.

Рассмотрим следующее

type And (a :: Constraint) b = (a, b)

или сложнее

class (a, b) => And a b
instance (a, b) => And a b

Я хочу знать, как логически или два ограничения вместе в Haskell.

Моя ближайшая попытка - это, но это не совсем работает. В этой попытке я повторяю ограничения типов с тегами и чем их разделяют с неявными параметрами.

data ROr a b where
 L :: a => ROr a b
 R :: b => ROr a b

type Or a b = (?choose :: ROr a b)

y :: Or (a ~ Integer) (Bool ~ Integer) => a
y = case ?choose of
 L -> 4

x :: Integer
x = let ?choose = L in y

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

Как я могу логически или два ограничения вместе?

Ответы

Ответ 1

Я считаю, что нет возможности автоматически выбрать ROr a b; это нарушало бы предположение открытого мира, если, например, b было выполнено, но позже a было выполнено; любое правило разрешения конфликтов обязательно приведет к добавлению экземпляра для изменения поведения существующего кода.

То есть, выбор R, когда b выполняется, но a не нарушает предположения открытого мира, поскольку он предполагает принятие решения о том, что экземпляр не выполняется; 1 даже если вы добавлен конструктор "оба удовлетворены", вы сможете использовать его, чтобы решить, нет ли экземпляра (если вы видите L или R).

Поэтому я не считаю, что такое ограничение или ограничение возможно; если вы можете наблюдать, какой экземпляр вы получаете, то вы можете создать программу, поведение которой изменяется путем добавления экземпляра, и если вы не можете наблюдать, какой экземпляр вы получаете, то это довольно бесполезно.

1 Различие между этим и нормальным разрешением экземпляра, которое также может потерпеть неудачу, заключается в том, что, как правило, компилятор не может решить, что ограничение выполнено; здесь вы просите компилятор решить, что ограничение не может быть выполнено. Тонкая, но важная разница.