[grumpyprole]

Yes, but like any encoding, it has its problems. One potential issue is that you will need to formulate your transformations as strict catamorphisms (folds), e.g. you cannot match two levels deep. This has reasoning advantages, but makes it harder for the average user. Type classes can also have issues with ambiguities, if many type variables are involved. Lastly, you also cannot match all remaining terms, like these examples:

  getDates
      :: Exp 
      -> Set Date
  getDates = cata alg where
    alg :: ExpF (Set Date) -> Set Date
    alg (EDate i) = S.singleton i
    alg e = fold e

  substitute 
      :: Map VarId (ExpF Exp) 
      -> Exp
      -> Exp 
  substitute env = cata alg where
    alg :: ExpF Exp -> Exp 
    alg (EVar i) 
      | Just e <-M.lookup i env = Fix e 
    alg e = Fix e

[siraben]

Ah ha, but you see, you can perform transformations on tagless-final terms that are not strict catamorphisms. Oleg demonstrates this in (page 14)[0] with examples of reassociating binary expressions and double negation, so matching two levels deep is possible.

As for matching remaining terms, I don't know the answer to that, would be interesting to investigate.

Yeah, having many typeclasses involved could be problematic. What sort of issues are you thinking of? One possibility is that so many constraints are involved no concrete type can instantiate a final term.

[0] http://okmij.org/ftp/tagless-final/course/lecture.pdf

[willtim]

> Ah ha, but you see, you can perform transformations on tagless-final terms that are not strict catamorphisms ... so matching two levels deep is possible.

No this is not correct. Oleg provides a solution to double negation by creating a catamorphism that folds to a function. It's still a catamorphism. And folding to a function is not something the average Java programmer is likely to understand easily.

[siraben]

Right, so it's not that it's not possible but rather it's somewhat awkward to express non-compositional folds in the final approach. I'm not currently aware of a mechanical way to do the translation.

[willtim]

Yes, I'm claiming the restriction will be too much for many people, assuming we are trying to create a new language here. However, expressing a solution as a catamorphism is a good thing to do and helps reasoning. It's a form of structured programming (recursion is the "goto" of functional programming!).