Wie kann ich in Haskell ein m-ary-Prädikat und ein n-ary-Prädikat nehmen und ein (m + n) -äres Prädikat konstruieren?

Question

Heute spielte ich mit der Verwendung von Typklassen, um induktiv Funktionen eines Prädikats jeder Art zu konstruieren, die als Eingabe eine beliebige Kombination beliebiger Typen verwenden, die andere Prädikate des gleichen Typs, aber mit einigen grundlegenden Operationen, zurückgegeben haben. Zum Beispiel

conjunction (>2) even 

zurückkehren würde ein Prädikat, das für gerade Zahlen größer als zwei und

conjunction (>=) (<=) 

zurückkehren würde =

Alles schön und gut, bekam, dass ein Teil arbeiten, aber es wahr ergibt die Frage aufgeworfen, was wäre, wenn ich die Konjunktion zweier Prädikate als ein Prädikat definieren möchte, das für jede Eingabe jedes verbundenen Prädikats eine Eingabe benötigt? Zum Beispiel:

:t conjunction (>) not 

zurückkehren würde Ord a => a -> a -> Bool -> Bool. Kann das gemacht werden? Wenn das so ist, wie?

Answer 1

Wir werden TypeFamilies für diese Lösung benötigen.

{-# LANGUAGE TypeFamilies #-} 

Die Idee ist, eine Klasse Pred für n-stellige Prädikate zu definieren:

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

Das Problem dreht sich alles um wieder schlurfenden Argumente zu den Prädikaten, so ist dies, was die Klasse zielt darauf ab, zu tun . Der zugehörige Typ Arg soll Zugriff auf die Argumente eines n-stelliges Prädikat geben, indem die endgültige Bool mit k zu ersetzen, so dass, wenn wir eine Art

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

dann haben

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

Dies ermöglicht Wir erstellen den richtigen Ergebnistyp von conjunction, in dem alle Argumente der beiden Prädikate gesammelt werden sollen.

Die Funktion split nimmt ein Prädikat des Typs a und eine Fortsetzung des Typs Bool -> r und wird etwas vom Typ Arg a r produzieren. Die Idee von split ist, dass, wenn wir wissen, was mit der Bool zu tun ist, wir aus dem Prädikat am Ende erhalten, dann können wir andere Dinge (r) dazwischen tun.

Es überrascht nicht, wir werden zwei Instanzen benötigen, eine für Bool und eine für Funktionen, für die das Ziel bereits ein Prädikat:

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

A Bool keine Argumente hat, so Arg Bool k einfach k zurückgibt.Auch für split haben wir die Bool bereits, so dass wir sofort die Fortsetzung anwenden können.

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

Wenn wir ein Prädikat vom Typ a -> r haben, dann Arg (a -> r) k müssen mit a -> beginnen, und wir werden weiterhin durch Arg rekursiv auf r aufrufen. Für split können wir nun drei Argumente annehmen, wobei x vom Typ a ist. Wir können x zu f führen und dann split auf das Ergebnis aufrufen.

Sobald wir die Pred Klasse definiert haben, ist es leicht, conjunction zu definieren:

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

Die Funktion nimmt zwei Prädikate und gibt etwas vom Typ Arg a (Arg b Bool). Schauen wir uns das Beispiel an:

GHCi erweitert diesen Typ nicht, aber wir können. Der Typ entspricht

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

was genau wir wollen. Wir können eine Reihe von Beispielen testen, zu:

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

Beachten Sie, dass die Pred Klasse verwenden, ist es trivial ist, andere Funktionen zu schreiben (wie disjunction) auch.

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 

Ich hoffe, es ist selbsterklärend, aber wenn nicht, zögern Sie nicht, Fragen zu stellen.

Auch könnten Sie die beiden Klassen natürlich zu einem zusammenführen, aber ich fühle, dass die zwei Klassen die Idee klarer machen.