CODEWITHSUNDEEP
haskellpattern-matchingtypeclassrecursive-datastructures
Sven Williamson
Sven Williamson

Reputation: 1124

How to pattern match against typeclass whose instance are recursive data types?

This question is a follow up on How to pattern match against a typeclass value?.

I am starting up a pet project on first order logic and have decided to use Haskell for this purpose. My first hurdle is to define a 'formula of first order logic', hence the data type:

data Formula v  = Belong v v                      -- x in y
                | Bot                             -- False
                | Imply (Formula v) (Formula v)   -- p -> q
                | Forall v (Formula v)            -- forall x, p

However, I am reluctant to write code based on the implementation specifics, and would rather abstract away the details, in case I change my mind, or in case I want to reuse functionality with an alternative implementation, hence the typeclass:

class FirstOrder m where
  belong    :: v -> v -> m v
  bot       :: m v
  imply     :: m v -> m v -> m v
  forall    :: v -> m v -> m v
  asFormula :: m v -> Formula v

I have added the last function asFormula in order to use the ViewPatterns (as suggested in the above link), so as to be able to pattern match on values of this typeclass.

Now suppose I want to define a simple function:

subst :: (FirstOrder m) => (v -> w) -> m v -> m w

which substitutes variables in a formula as per a given mapping f::v -> w (feels like fmap), so the formula belong x y is mapped to belong (f x) (f y) etc. then using ViewPatterns:

subst f (asFormula -> Belong x y) = belong (f x) (f y)

so far so good...

However, when attempting to write subst f p->q = (subst f p) -> (subst f q):

subst f (asFormula -> Imply p q)  = imply (subst f p) (subst f q)

I get a type error, which coming to think of it makes perfect sense: the pattern matching binds p and q to elements of type Formula v as opposed to the desired type m v.

Now I can see the problem, and could even think of ways of solving it by adding a fromFormula function to the typeclass to convert back to the type m v, but I am thinking this is crazy from a performance point of view (just as crazy as asFormula mind you), a huge price to pay in order to keep the code generic.

So here I am now, trying to define a simple function by structural recursion on a free algebra (recursive data type), but my desire to abstract away the implementation details (and write code off typeclass rather than data type) is putting me in what seems to be an impossible position.

Is there a way out, or should I just forget about abstraction and work with the recursive data type?

Upvotes: 2

Views: 401

Answers (1)

chi
chi

Reputation: 116139

This looks as an overgeneralization, but let's ignore that anyway.

You can solve that with explicit F-(co-)algebras and fixed points.

data FormulaF v k
   = Belong v v                      -- x in y
   | Bot                             -- False
   | Imply (k v) (k v)               -- p -> q
   | Forall v (k v)                  -- forall x, p

newtype Formula v = Formula (FormulaF v Formula)      
   -- fixed point. You might not need it, but it's nice to have.
   --

Then, you can do

class FirstOrder m where
  belong    :: v -> v -> m v
  bot       :: m v
  imply     :: m v -> m v -> m v
  forall    :: v -> m v -> m v
  asFormula :: m v -> FormulaF v m

and

subst :: (FirstOrder m) => (v -> w) -> m v -> m w
subst f (asFormula -> Belong x y) = belong (f x) (f y)
subst f (asFormula -> Imply p q)  = imply (subst f p) (subst f q)

should now work, because asFormula does not convert the whole m v into a full formula recursively, but it converts into a FormulaF v m which looks as a formula superficially (the very first constructor you pattern match, like Imply), but deep inside still looks as a m v.

If you really want to pursue this overgeneral approach, maybe you should have a look at recursion-schemes, F-algebras and F-coalgebras, and their associated cata-/ana-/hylo-/para-/whatever morphisms.

Finally, I would suggest to avoid trying to adapt OOP design patterns in FP. Sometimes you can shoehorn something in such way, but it can often be unidiomatic. For instance, in Haskell, we are quite used to types having a fixed amount of constructors (but an open set of functions which operate on them), just like in OOP interfaces have a fixed amount of methods (but an open set of subclasses). One can try to generalize this, but it's complex, and should be done only when needed.

Upvotes: 2

Related Questions