How can I use `bound` for non-monads?

Question

I am trying to use the bound package to represent terms and propositions in a simple logical language. Here is what I have so far:

import Bound

data Term a = V a
            | Func String [Term a]
  deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable)

data Prop a = And (Prop a) (Prop a)
            | Relation String [Term a]
            | Forall (Scope () Prop a)
            deriving (Functor, Foldable, Traversable)

In particular, there are terms which are either variables, or functions applied to some terms, as well as propositions which are: conjunction of two propositions, a relation applied to some terms, and quantification over variables in another proposition. But when I try to create a function to construct a "Forall", following the example in the package documentation, I am told that Prop is not a monad:

forall' :: Eq a => a -> Prop a -> Prop a
forall' v b = Forall (abstract1 v b)

This is expected, since I didn't define Monad Prop. But there is no sensible pure (or return) into Prop, so how can I support this language using the bound package?

user_246886 · Answer

I think you just need to merge Term and Prop here:

data Exp a
  = V a
  | Func String [Exp a]
  | And (Exp a) (Exp a)
  | Relation String [Exp a]
  | Forall (Scope () Prop a)

If I understand correctly, the Applicative/Monad structure that abstract1 wants is supposed to have pure inject a variable and >>= do substitution. With this, your Applicative and Monad instances can straightforwardly follow the documentation:

instance Applicative Exp where
  pure = V
  (<*>) = ap

instance Monad Exp where
  return = V
  V a           >>= f = f a
  And x y       >>= f = And (x >>= f) (y >>= f)
  Relation r xs >>= f = Relation r (fmap (>>= f) xs)  -- (I think.)
  Forall e      >>= f = Forall (e >>>= f)             -- NB: bound’s ‘>>>=’.

You can rearrange this in different ways depending on your use case:

Adding a constructor to Prop wrapping a single Term:

data Prop a
  = And (Prop a) (Prop a)
  | Relation String [Term a]
  | Forall (Scope () Prop a)
  | Term (Term a)

Making Exp a sum of Term or Prop and implementing Applicative & Monad for that:
```
data Exp a
  = Term (Term a)
  | Prop (Prop a)
```

Making Exp a GADT indexed by whether it’s an atomic term or a general proposition:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Class = Atomic | Compound

data Exp (c :: Class) a where
  V        :: a                  -> Term a
  Func     :: String -> [Term a] -> Term a
  And      :: Prop a -> Prop a   -> Prop a
  Relation :: String -> [Term a] -> Prop a
  Forall   :: Scope () Prop a    -> Prop a

type Term a = Exp 'Atomic a
type Prop a = Exp 'Compound a

Making newtype wrappers with smart constructors for the “subtypes” of Exp if you only need to differentiate them sometimes:

newtype Term a = Term (Exp a)
newtype Prop a = Prop (Exp a)

term :: Exp a -> Maybe (Term a)
term t = case t of
  V{}    -> yes
  Func{} -> yes
  _      -> no
  where
    yes = Just (Term t)
    no  = Nothing

prop :: Exp a -> Maybe (Prop a)
prop t = case t of
  …

But whichever way, you need V in there to express “propositions can be variables” or “expressions can be either propositions or variables”. In fact, I think you could actually express that with your type as-is, using a dummy relation: pure a = Relation "" [V a], but one of these other forms is probably cleaner.

How can I use `bound` for non-monads?

1 Answers