I'm pretty sure I can show that, in principle, the `Predicate` type constructor is a `ContraMonad`, a generalization of `Monad` where the functor is contravariant, but I'm not sure how it would be implemented.

First, let's define some terms: 

```
class Contravariant f where
    contramap :: (b -> a) -> f a -> f b

class ContraMonad m where
    return :: a -> m a
    join :: m(m a) -> m a
    contrabind :: m a -> (m b -> a) -> m b

data Predicate a = Pred {getPred :: a -> Bool}

instance Contravariant Predicate where
    contramap f x = Pred ((getPred x).f)

```

This shows that a predicate, which is a function that takes values of a and generates propositions from them, is a contravariant functor from Hask to Hask^{op}. An example of a predicate would be:

```
isEven :: Integer -> Bool
isEven n = if (mod n 2 == 0)
           then True
           else False

```

The function `isEven` is a predicate in the mathematical sense, while `Pred isEven` is a `Predicate` in the sense implemented here.

Implementing `Predicate` as a `ContraMonad` is trickier.

There is only one natural choice for `return`.

```
return :: a -> Predicate a
return x = Pred(const True)

```

You may consider the possibility of 'return' giving a Predicate for which x is true and no other elements of type a are true. The problem is that this can only be implemented if a is a member of the `Eq` typeclass.

It is easier to think about join than `contrabind`. Clearly, we want

```
contrabind x f = join.contramap f x

```

so that contrabind resembles bind as much as possible while taking account of f as a contravariant functor. The function `f` takes `Pred b` to `a`, so `contramap f` takes `Pred a` to `Pred(Pred b)`.

So, what should `join` do? It must take a Predicate of a Predicate of type a to a Predicate of type a. A Predicate of a Predicate of type a makes a judgement about predicates of type a. As an example, consider a = Integer. An example of `Pred( Pred Integer)` is:

```
Pred("The predicate f is true for all even numbers.")

```

Where I have used a quote in place of an actual implementation. If it is the case that f is true for all evens, then this statement is true. For example, `Pred isEven` would evaluate to `True`.

Considering the fact that predicates on a set A are correspond to subsets of A, a `Pred(Pred A)` is a wrapper for a function that takes all subsets of A and judges them as "True" or "False." We want `join` to give us a predicate, which is the same as giving a subset of A. This subset should be as lossless as possible. In fact, it should care about the truth value of every single `Pred X`, w.r.t. the `Pred(Pred X)` judgment. The natural solution seems, to me, to be the intersection of all subsets judged as "True," which is the same thing as "ANDing" together all true predicates where

```
predAnd :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
predAnd p q = \x -> ((getPred p) $ x) && ((getPred q) $ x)

```

As an example, let's go back to "The predicate f is true for all even numbers." Every predicate evaluated as `True` under this judgment must be true for all evens, so every possible subset contains the evens. The intersection of all these sets will simply be the set of evens, so `join` would return the predicate `Pred isEven`.

My question is this, how would 'join' actually be implemented? Can it be implemented? I can see potential problems with undecidable sets arising for infinite types like 'Integer', but could it even be implemented for finite types like 'Char', where even the power set has finite cardinality?