W Haskell, jak mogę wziąć predykat m-ary i predykat n-ary i skonstruować (m + n) -aryfikat predykatu?

Question

Dzisiaj grałem z wykorzystaniem klas typów do indukcyjnego konstruowania funkcji predykatu dowolnej arii, przyjmując jako dane wejściowe dowolną kombinację dowolnych typów, które zwróciły inne predykaty tego samego typu, ale z pewną podstawową operacją. Na przykład

conjunction (>2) even 

zwróci orzeczenie, że wartość true dla parzystych numerach większych niż dwa i

conjunction (>=) (<=) 

wróci =

Wszystko dobrze, got, że praca w niepełnym wymiarze, ale to postawił pytanie, co jeśli chciałbym zdefiniować koniunkcję dwóch predykatów jako predykat, który bierze jeden wkład dla każdego wejścia każdego zrośniętego predykatu? Na przykład:

:t conjunction (>) not 

zwróci Ord a => a -> a -> Bool -> Bool. Czy można to zrobić? Jeśli tak to jak?

Answer 1

Będziemy potrzebować TypeFamilies dla tego rozwiązania.

{-# LANGUAGE TypeFamilies #-} 

Chodzi o to, aby zdefiniować klasę Pred dla n-arnych predykatów:

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

Problem jest o argumentach ponownie tasowania do orzeczników, więc to, co ma klasa zrobić . Powiązany typ Arg ma dać dostęp do argumentów n-ary orzecznika zastępując końcowy Bool z k, więc jeśli mamy typ

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

następnie

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

To pozwoli nam zbudować odpowiedni typ wyniku: conjunction, gdzie wszystkie argumenty z dwóch predykatów mają być zebrane.

Funkcja split pobiera predykat typu a i kontynuację typu Bool -> r i wygeneruje coś typu Arg a r. Pomysł na split polega na tym, że jeśli wiemy, co zrobić z Bool, które uzyskujemy z predykatu na końcu, możemy zrobić między innymi inne rzeczy (r).

Nic dziwnego, że musimy dwa przypadki, jeden dla Bool i jeden dla funkcji, dla których cel jest już orzeczenie:

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

Bool ma żadnych argumentów, więc Arg Bool k prostu zwraca k.Również dla split mamy już Bool, więc możemy od razu zastosować kontynuację.

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

Jeśli mamy predykat typu a -> r, następnie Arg (a -> r) k musi zaczynać się a ->, a my nadal wywołując Arg rekurencyjnie na r. W przypadku split możemy teraz przyjąć trzy argumenty: x będący typu a. Możemy podać x do f, a następnie wywołać split na wyniku.

Po zdefiniowaniu klasy Pred, to jest łatwe do zdefiniowania conjunction:

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

Funkcja przyjmuje dwa predykaty i zwraca coś typu Arg a (Arg b Bool). Spójrzmy na przykład:

GHCi nie rozszerza tego typu, ale możemy. Typ jest równoważny z

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

który jest dokładnie tym, czego chcemy. Możemy przetestować szereg przykładów, za:

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

Należy pamiętać, że przy użyciu klasy Pred, to jest trywialne napisać inne funkcje (np disjunction), też.

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 

Mam nadzieję, że to nie wymaga objaśnień, ale jeśli nie, proszę zadawać pytania.

Oczywiście, możesz połączyć dwie klasy w jedną, oczywiście, ale wydaje mi się, że te dwie klasy sprawiają, że idea jest bardziej przejrzysta.