Implementing predicate types as contravariant monads?

Question

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?

I noticed that `\f x -> contrabind (return x) f :: (m b -> a) -> a -> m b`. Somehow I don't like how we can flip the direction of these functions: every contramonad must support that, which seems hard to achieve. Also, `contrabind (return ()) (const ()) : m b` for any `b` looks quite weird. — chi, Sep 07 '17 at 07:53
https://stackoverflow.com/questions/30641500/are-there-contravariant-monads — Cirdec, Sep 07 '17 at 08:28
The function is flipped because m is a contravariant functor. Thus, a function from `m b -> a` becomes a function from `m a -> m (m b))`. Every contramonad can achieve this as long as it is contravariant instead of covariant. You can write `contrabind x f = join.contramap (f x)`. The `contramap f` function almost always works by precomposing with f as opposed to the normal postcomposition with f. That's how most contravariant functors work. A `ContraMonad` should be exactly like a `Monad` except for the fact that it's contravariant. Thus, `return` and `join` shouldn't change. — E8xE8, Sep 08 '17 at 00:06

Cirdec · Answer 1 · 2017-09-07T10:26:24.513

3

There is something related, the contravariant version of Applicative is Divisible, which I've simplified here

class Contravariant f => Divisible f where
  divide  :: f b -> f c -> f (b, c)
  conquer :: f a

The divide in Data.Functor.Contravariant.Divisible is written in terms of a -> (b, c) which highlights the idea of dividing the work for a into the work for b and c.

{-# LANGUAGE RankNTypes #-}

-- The divide from Data.Functor.Contravariant.Divisible
divide' :: Divisible f => (a -> (b, c)) -> f b -> f c -> f a
divide' f b c = contramap f $ divide b c

-- And a proof they types are equivalent
proof :: (forall a b c. (a -> (b, c)) -> f b -> f c -> f a) -> f b -> f c -> f (b, c)
proof divide' = divide' id

Any Op is Divisible if its result is a Monoid. This is a generalization of Predicate, which is Op All

import Data.Monoid

newtype Op r a = Op {runOp :: a -> r}

instance Contravariant (Op r) where
  contramap f (Op g) = Op (g . f)

instance Monoid r => Divisible (Op r) where
  divide (Op f) (Op g) = Op (\(b, c) -> f b <> g c)
  conquer = Op (const mempty)

As a bonus, Op r is a Monoid as long as the result r is a moniod, which provides a straightforward way to define predAnd

instance Monoid a => Monoid (Op a b) where
  mempty = Op (const mempty)
  mappend (Op p) (Op q) = Op $ \a -> mappend (p a) (q a)

type Predicate a = Op All a

predAnd :: Predicate a -> Predicate a -> Predicate a
predAnd = mappend

But that's hardly surprising.

edited Sep 07 '17 at 10:26

answered Sep 07 '17 at 10:19

Cirdec

24,019
2
50
100

So, if I may ask, what would `join` be for `Predicate`? Is it possible to write the code implementing `join :: Predicate (Predicate a) -> Predicate a` in Haskell? If so, what is that code? – E8xE8 Sep 08 '17 at 00:14
`Predicate (Predicate a)` is `(a -> Bool) -> Bool`. There's no way to convert that to `a -> Bool`. An `a -> Bool` is exactly what you need to get anything non-trivial out of `(a -> Bool) -> Bool`! – Cirdec Sep 08 '17 at 02:43
So there's no way to take the `predAnd` of all possible predicates in `Predicate( Predicate a)`? I know it might not be possible to implement in Haskell, but at least in theory, it can be calculated in many cases. It can always be calculated if a is a finite set. – E8xE8 Sep 08 '17 at 03:39
Try it for a small data type, like `a ~ Word8` – Cirdec Sep 08 '17 at 08:46
I have some ideas, but there's not enough room to type them all here. First, we would need to require the `a` in `Pred a` to be in the `Eq` typeclass. Then, we can find a way to define `Pred a` as being in `Eq` by saying two predicates are equal if and only if they are true for exactly the same terms of `a`. Finally, we could construct a new data type, `data Remove a = Rmv {getRmv :: [a]}` which represents the data type `a` with the elements of the list being removed. This would allow us to recursively call `join`, removing each predicate from `Pred a` one at a time. – E8xE8 Sep 09 '17 at 23:27
That's not the problem. Check out the universe package, it defines equality for types with finite universes. The problem is that once you start considering all possible predicates `a -> Bool` the number of predicates is `2^a`. So computing all the predicates to see if they're admitted by `Predicate (Predicate a)` would take on the order of 2^256 steps when `a` is an 8 bit word. – Cirdec Sep 10 '17 at 01:20
If you replace the predicates with sets then sets are an ordinary monad where join is set union. You need something like [`constrained-categories`](https://github.com/leftaroundabout/constrained-categories), because you need an `Ord a` or at least `Eq a` constraint to join `Set (Set a)` into `Set a`. – Cirdec Sep 10 '17 at 01:22

score 0 · Answer 2 · answered Sep 10 '17 at 07:47

I think I may have thought of a partial answer to my own question. First, we must force a to be in the Eq typeclass.

join p = Pred(\x -> not ((getPred p) (\y -> y /= x)))

This is a predicate which takes an element of type a and constructs a predicate out of it, namely the predicate where x is false and everything else is true. Then, it evaluates this predicate according to the original Pred( Pred a) judgment.

If this predicate is true, than it is the case that x is not in the intersection of all predicates, and thus the final predicate sends x to False. On the other hand, if this predicate is false, it is not necessarily the case that x is in the intersection, unless we make an additional rule:

If the Pred( Pred a) judgment rules a nearly maximal predicate false, the element ruled false in the nearly maximal predicate must appear in all predicates judged to be true.

Thus, the judgment "The predicate f is true for all even numbers." is allowed under this rule, but the judgment "The predicate f is true only for even numbers." is not allowed. If a judgment of the first kind is used, join will give the intersection of all true predicates. In the second case, join will simply give a predicate which can sometimes tell you if x is unnecessary. If it returns False, x is definitely unnecessary. If it returns True, the test is inconclusive.

I'm now convinced that a full implementation of "ANDing" is impossible unless the type a is finite and even then is impractical unless a is very small.

As an addendum, another very natural operator, which gives the union of all true predicates would be `isSufficient :: Predicate( Predicate a) -> Predicate a` where `isSufficient p = Pred(\x -> (getPred p) (\y -> y == x))`. This would let you know if `x` is sufficient for a predicate to be judged as true. Unlike necessity, this is straightforward to implement and requires no additional rules. — E8xE8, Sep 10 '17 at 07:49

Implementing predicate types as contravariant monads?

2 Answers2