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

Question

В 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 

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

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

Answer 1

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

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

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

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