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?

Accepted Answer

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.

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

Solution

Problem