Make constrained functions a typeclass instance

Question

I'm relatively new to Haskell so I apologise if I'm not getting the terminology completely correct.

I'm trying to write an implementation of Linear Temporal Logic using Haskell where an expression can be constructed and then applied to a list of elements to produce a Boolean result using a function with the following signature:

evaluate :: Expression a -> [a] -> Bool

With Expression a being an algebraic data type defined something like this:

data Expression a = Conjunction (Expression a) (Expression a)
                  | Disjunction (Expression a) (Expression a)
                  | Next (Expression a)
                  | Always (Expression a)
                  | Eventually (Expression a)
                  | Until (Expression a) (Expression a)
                  | Predicate (a -> Bool)
                  -- etc. etc.

This all works fine, but I'd like to make constructing expressions a little more elegant by defining smart constructors, ideally that could be used something a little like this:

numExpr :: Num a => Expression a
numExpr = eventually (== 10) `or` eventually (== 5)

So far my attempts at achieving this have involved something like the following:

eventually :: Expressable e => e a -> Expression a
eventually = Eventually . expresss

or :: (Expressable e, Expressable f) => e a -> f a -> Expression a
or x y = Or (express x) (express y)

-- and so on

class Expressable e where
  express :: e a -> Expression a

instance Expressable Expression where
  express = id

-- This is what I'd like to do:

type Pred a = a -> Bool

instance Expressable Pred where
  express = Predicate

However the latter doesn't work. I've tried using various GHC extensions (LiberalTypeSynonyms, TypeSynonymInstances) but nothing has seemed to work. Is this kind of thing possible or even a good idea? Is there a good reason why the type system will not allow this kind of thing? Is there a better way to structure this that would work?

I know I could use a short function name with a signature like p :: (a -> Bool) -> Expression a but this still feels a little inelegant.

Answer 1

A newtype instead of type would work:

newtype Pred a = Pred (a -> Bool)

instance Expressable Pred where
  express (Pred p) = Predicate p

In your case, Pred in instance Expressable Pred where is a partially applied type synonym and those are basically never allowed (see LiberalTypeSynonyms for the exception).

Answer 2

In your approach you need to link the a which is the argument of Pred to the a in the signature of express. These have to be the same, but you can't require that in your class / instances.

You can however try something like this, with a bunch of extensions on:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

data Expression a = Conjunction (Expression a) (Expression a)
                  | Disjunction (Expression a) (Expression a)
                  | Next (Expression a)
                  | Always (Expression a)
                  | Eventually (Expression a)
                  | Until (Expression a) (Expression a)
                  | Predicate (a -> Bool)

class Expressable e a where
      express :: e -> Expression a
    
instance Expressable (Expression a) a where
  express = id

type Pred a = a -> Bool

instance Expressable (Pred a) a where
  express = Predicate

eventually :: Expressable e a => e -> Expression a
eventually = Eventually . express

or :: (Expressable e a, Expressable f a) => e -> f -> Expression a
or x y = Disjunction (express x) (express y)

I'm not terribly convinced it is a good idea to use such machinery only to avoid writing Predicate on the atomic formulae, but you might give it a whirl and see if it works well enough in practice.