In Haskell come posso prendere un predicato m-ary e un predicato n-ary e costruire un predicato -ar (m + n) -are?

Question

Oggi ho giocato con le classi di tipi per costruire in modo induttivo le funzioni di un predicato di qualsiasi organizzazione prendendo come input qualsiasi combinazione di qualsiasi tipo, che restituiva altri predicati dello stesso tipo ma con alcune operazioni di base applicate. Per esempio

conjunction (>2) even 

restituirebbe un predicato che restituisce true anche per i numeri più grandi di due e

conjunction (>=) (<=) 

sarebbero tornati =

Tutto bene, ha ottenuto che il lavoro parte, ma sollevato la domanda, e se volessi definire la congiunzione di due predicati come un predicato che prende un input per ogni input di ogni predicato congiunto? Per esempio:

:t conjunction (>) not 

sarebbe tornare Ord a => a -> a -> Bool -> Bool. Può essere fatto? Se é cosi, come?

Answer 1

Avremo bisogno di TypeFamilies per questa soluzione.

{-# LANGUAGE TypeFamilies #-} 

L'idea è di definire una classe Pred per predicati n-ari:

class Pred a where 
    type Arg a k :: * 
    split :: a -> (Bool -> r) -> Arg a r 

Il problema è tutto su argomenti rimescolamento ai predicati, quindi questo è ciò che il corso si propone di fare . Il tipo associato Arg dovrebbe dare accesso agli argomenti di un predicato n-ario sostituendo il finale Bool con k, quindi se abbiamo un tipo

X = arg1 -> arg2 -> ... -> argn -> Bool 

poi

Arg X k = arg1 -> arg2 -> ... -> argn -> k 

Ciò consentirà per costruire il tipo di risultato corretto di conjunction in cui devono essere raccolti tutti gli argomenti dei due predicati.

La funzione split prende un predicato di tipo a e una continuazione di tipo Bool -> r e produrrà qualcosa di tipo Arg a r. L'idea di split è che se sappiamo cosa fare con il Bool otteniamo dal predicato alla fine, quindi possiamo fare altre cose (r) in mezzo.

Non a caso, avremo bisogno di due istanze, una per Bool e uno per le funzioni per le quali l'obiettivo è già un predicato:

instance Pred Bool where 
    type Arg Bool k = k 
    split b k = k b 

Un Bool non ha argomenti, in modo Arg Bool k semplicemente restituisce k.Inoltre, per split, abbiamo già lo Bool, quindi possiamo applicare immediatamente la continuazione.

instance Pred r => Pred (a -> r) where 
    type Arg (a -> r) k = a -> Arg r k 
    split f k x = split (f x) k 

Se abbiamo un predicato di tipo a -> r, quindi Arg (a -> r) k deve iniziare con a ->, e continuiamo chiamando Arg ricorsivamente su r. Per split, ora possiamo prendere tre argomenti, il x è di tipo a. Possiamo alimentare x a f e quindi chiamare split sul risultato.

Una volta che abbiamo definito la classe Pred, è facile definire conjunction:

conjunction :: (Pred a, Pred b) => a -> b -> Arg a (Arg b Bool) 
conjunction x y = split x (\ xb -> split y (\ yb -> xb && yb)) 

La funzione prende due predicati e restituisce qualcosa di tipo Arg a (Arg b Bool). Guardiamo l'esempio:

> :t conjunction (>) not 
conjunction (>) not 
    :: Ord a => Arg (a -> a -> Bool) (Arg (Bool -> Bool) Bool) 

GHCi non si espande questo tipo, ma possiamo. Il tipo è equivalente a

Ord a => a -> a -> Bool -> Bool 

che è esattamente quello che vogliamo. Siamo in grado di testare una serie di esempi, anche:

> conjunction (>) not 4 2 False 
True 
> conjunction (>) not 4 2 True 
False 
> conjunction (>) not 2 2 False 
False 

Si noti che utilizzando la classe Pred, è banale scrivere altre funzioni (come disjunction), anche.

Answer 2

{-# LANGUAGE TypeFamilies #-} 

class RightConjunct b where 
    rconj :: Bool -> b -> b 

instance RightConjunct Bool where 
    rconj = (&&) 

instance RightConjunct b => RightConjunct (c -> b) where 
    rconj b f = \x -> b `rconj` f x 

class LeftConjunct a where 
    type Ret a b 
    lconj :: RightConjunct b => a -> b -> Ret a b 

instance LeftConjunct Bool where 
    type Ret Bool b = b 
    lconj = rconj 

instance LeftConjunct a => LeftConjunct (c -> a) where 
    type Ret (c -> a) b = c -> Ret a b 
    lconj f y = \x -> f x `lconj` y 

conjunction :: (LeftConjunct a, RightConjunct b) => a -> b -> Ret a b 
conjunction = lconj 

Spero che sia auto-esplicativo, ma in caso contrario, non esitate a fare domande.

Inoltre, è possibile unire le due classi in una, ovviamente, ma sento che le due classi rendono l'idea più chiara.