3 ms·

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.

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 6y ago
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 http://okmij.org/ftp/tagless-final/course/lecture.pdf
- willtim 6y ago
  > 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 6y ago
    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 6y ago
      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!).

siraben 6y ago

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 http://okmij.org/ftp/tagless-final/course/lecture.pdf

willtim 6y ago
> 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 6y ago
  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 6y ago
    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!).