In Haskell, how can I take the m-ary predicate and n-ary predicate and build the (m + n) -principal predicate?

Question

Today I played using type classes to inductively construct predicate functions of any arity, taking as an attachment any combination of any types that returned other predicates of the same type, but applied some basic operation. for example

conjunction (>2) even 

will return a predicate that evaluates to true for even numbers greater than two, and

 conjunction (>=) (<=) 

will return =

All is well and good, that this part works, but it posed the question, what if I wanted to define a join of two predicates as a predicate that takes one input for each input of each combined predicate? For example:

 :t conjunction (>) not 

will return Ord a => a → a → Bool → Bool. It can be done? If so, how?

Answer 1

We will need TypeFamilies for this solution.

 {-# LANGUAGE TypeFamilies #-} 

The idea is to define a Pred class for n-ary predicates:

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

The problem is re-shuffling the arguments into predicates, so this is what the class should do. The associated Arg type should provide access to the arguments of the n-ary predicate, replacing the final Bool with k , so if we have a type

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

then

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

This will allow us to construct the correct type of conjunction result, where all arguments of the two predicates should be collected.

The split function takes a predicate of type a and extensions of type Bool -> r and Arg ar something like Arg ar . The idea of split is that if we know what to do with Bool , we get from the predicate at the end, then we can do other things ( r ) between them.

It is not surprising that we will need two instances: one for Bool and one for functions for which the target is already a predicate:

 instance Pred Bool where type Arg Bool k = k split bk = kb 

A Bool has no arguments, so Arg Bool k just returns k . In addition, for split we already have Bool , so we can immediately apply the continuation.

 instance Pred r => Pred (a -> r) where type Arg (a -> r) k = a -> Arg rk split fkx = split (fx) k 

If we have a predicate of type a -> r , then Arg (a -> r) k should start with a -> , and we continue to call Arg recursively on r . For split we can now take three arguments, type x type a . We can send x to f and then call split as a result.

Once we have defined the Pred class, it is easy to define conjunction :

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

The function takes two predicates and returns something like Arg a (Arg b Bool) . Consider an example:

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

GHCi does not extend this type, but we can. Type equivalent

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

what we want. We can also check out a number of examples:

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

Note that using the Pred class Pred trivial to write other functions (e.g. disjunction ).

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 bf = \x -> b `rconj` fx class LeftConjunct a where type Ret ab lconj :: RightConjunct b => a -> b -> Ret ab 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 ab lconj fy = \x -> fx `lconj` y conjunction :: (LeftConjunct a, RightConjunct b) => a -> b -> Ret ab conjunction = lconj 

Hope this makes sense, but if not, feel free to ask questions.

In addition, you could combine the two classes into one, of course, but I feel that these two classes make the idea more clear.