Come posso combinare due vincoli di tipo con un logico o in Haskell?

Question

In Haskell ci viene data la possibilità di combinare i vincoli sui tipi con un logico e.

Si consideri il seguente

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

o più complicatamente

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

Voglio sapere come logicamente o due vincoli insieme in Haskell.

Il mio tentativo più vicino è questo, ma non funziona. In questo tentativo, reifaggo i vincoli di tipo con i tag e li cancello con parametri impliciti.

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 

Funziona quasi, ma l'utente deve applicare la parte finale e il compilatore dovrebbe farlo per me. Inoltre, questo caso non consente di scegliere una terza scelta quando entrambi i vincoli sono soddisfatti.

Come posso logicamente o due vincoli insieme?

Answer 1

Credo che non sia possibile selezionare automaticamente uno ROr a b; violerebbe l'ipotesi del mondo aperto se, ad es. b era soddisfatto, ma successivamente a era soddisfatto; qualsiasi regola di risoluzione dei conflitti causerebbe necessariamente l'aggiunta di un'istanza per modificare il comportamento del codice esistente.

Cioè, raccogliendo R quando b è soddisfatto, ma non è a rompe l'ipotesi mondo aperto, perché si tratta di decidere che un caso è non soddisfatti; anche se hai aggiunto un costruttore "entrambi soddisfatto", potresti utilizzarlo per decidere se un'istanza è non presente (vedendo se ottieni L o R).

Pertanto, non credo che tale vincolo o è possibile; se puoi osservare quale istanza ottieni, allora puoi creare un programma il cui comportamento cambia aggiungendo un'istanza e se non puoi osservare quale istanza ottieni, allora è abbastanza inutile.

La differenza tra questa e la normale risoluzione dell'istanza, che può anche non riuscire, è che normalmente il compilatore non può decidere che un vincolo è soddisfatto; qui, stai chiedendo al compilatore di decidere che il vincolo non può essere soddisfatto. Una differenza sottile ma importante.