In Haskell how can I take an m-ary predicate and an n-ary predicate and construct a (m+n)-ary predicate?

Question

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

conjunction (>2) even

would return a predicate that evaluates to true for even numbers larger than two and

conjunction (>=) (<=)

would return =

All well and good, got that part working, but it raised the question, what if I wanted to define conjunction of two predicates as being a predicate that takes one input for each input of each conjoined predicate? For example:

:t conjunction (>) not

would return Ord a => a -> a -> Bool -> Bool. Can this be done? If so, how?

Answer 1

We will need TypeFamilies for this solution.

{-# LANGUAGE TypeFamilies #-}

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

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

The problem is all about re-shuffling arguments to the predicates, so this is what the class aims to do. The associated type Arg is supposed to give access to the arguments of an n-ary predicate by 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 build the right result type of conjunction where all arguments of the two predicates are to be collected.

The function split takes a predicate of type a and a continuation of type Bool -> r and will produce something of type Arg a r. The idea of split is that if we know what to do with the Bool we obtain from the predicate in the end, then we can do other things (r) in between.

Not surprisingly, we'll 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 b k = k b

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

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

If we have a predicate of type a -> r, then Arg (a -> r) k must start with a ->, and we continue by calling Arg recursively on r. For split, we can now take three arguments, the x being of type a. We can feed x to f and then call split on the 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 x y = split x (\ xb -> split y (\ yb -> xb && yb))

The function takes two predicates and returns something of type Arg a (Arg b Bool). Let's look at the example:

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

GHCi doesn't expand this type, but we can. The type is equivalent to

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

which is exactly what we want. We can test a number of examples, too:

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

Note that using the Pred class, it is trivial to write other functions (like disjunction), too.

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

Hope it's self-explanatory, but if not, feel free to ask questions.

Also, you could merge the two classes into one, of course, but I feel that the two classes make the idea more clear.