How can I decide a free variable in a typeclass instance? (or how can I do recursion schemes for complex data structures?)

Learn
#1

Background

I am trying to set up something akin to recursion-schemes for a data structure that contains several mutually-recursive types as well as other type variables. In this simplified example, there are 4 pieces (“types”, “expressions”, “annotations”, and “namespaces”) representing an (incomplete) AST:

data Expression ns ann typ expr
  = Typed ann expr typ
  | Add ann expr expr
  | Literal ann Int
data Typ ns ann typ expr
  = Name ann ns String
  | Function typ [typ]

Then I’ve also defined fixpoints for “expressions” and “types” (with “namespaces” and “annotations” still parameterized):

newtype FTyp ns ann =
  FixT { unFixT :: Typ ns ann (FTyp ns ann) Never }
newtype FExpression ns ann =
  FixE { unFixE :: Expression ns ann (FTyp ns ann) (FExpression ns ann) }

And I’ve defined a typeclass for folding (cata) and unfolding (ana) the data structure (and successfully implemented instances for both FTyp and FExpression):

class MyClass fix where
  cata ::
    (ns -> ns')
    -> (ann -> ann')
    -> (Typ ns' ann' t' e' -> t')
    -> (Expression ns' ann' t' e' -> e')
    -> fix ns ann
    -> Either t' e'
  ana ::
    (ns' -> ns)
    -> (ann' -> ann)
    -> (t' -> Typ ns' ann' t' e')
    -> (e' -> Expression ns' ann' t' e')
    -> Either t' e'
    -> fix ns ann

You can find my current full working code here: https://repl.it/repls/ParchedWornOctagons

Question

I’d like to get rid of the Either t' e' in both functions – in instance MyClass FTyp, the Either will always be a Left value, and in instance MyClass FExpression, the Either will always be a Right value. Furthermore, it seems like it should always be clear from context which it will be; the choice of fix should determine whether it should be t' or e'. Is it possible to make a typeclass that allows for this?

If t' and e' were concrete types, I think something could be done with MultiParamTypeClasses and FunctionalDependencies, or TypeFamilies; but given they are universally quantified within each function, I’m not sure how to use either of those to any effect.

Other questions

I also realize that maybe I just shouldn’t be using a typeclass here and just define cataTyp/anaTyp/cataExpression/anaExpression separately. Would that be the preferred approach? (If so, I’d still be interested to know if it can be done with typeclasses).

For the general problem of writing reusable code that manipulates mutually-recursive, parameterized data types, is there are there better approaches I should be aware of? I’d be happy to receive any pointers to books, papers, libraries, examples, etc that cover this topic.

Thanks!

#2

Great question! Extending recursion schemes to these kinds of types can be tricky. There are two “fixes” (sorry for the horrible pun) I would mention – a simpler one for your code, and then a more general way of doing this.

  1. You can do this using type families. The trick is to use an associated type synonym in the MyClass declaration that “picks” which concrete type you want to use, based on the fix functor:

    class MyClass fix where
  type Pick fix t e :: *

  cata ::
    (ns -> ns')
    -> (ann -> ann')
    -> (Typ ns' ann' t' e' -> t')
    -> (Expression ns' ann' t' e' -> e')
    -> fix ns ann
    -> Pick fix t' e'

  ana ::
    (ns' -> ns)
    -> (ann' -> ann)
    -> (t' -> Typ ns' ann' t' e')
    -> (e' -> Expression ns' ann' t' e')
    -> Pick fix t' e'
    -> fix ns ann

    We can then write the instances as follows:

    instance MyClass FTyp where
  type Pick FType t e = t
  ...

instance MyClass FExpression where
  type Pick FExpression t e = e
  ...

    I updated this in a fork of your full code.

  2. I remember this problem being tackled quite elegantly in generic programming with fixed points for mutually recursive datatypes. It’s not an easy paper but seeing how far you got with your own solution I think you’ll manage! :slight_smile:

Hope this helps!

1 Like
#3

Thank you. Both answers were exactly what I was looking for!