Is there a name for mapping recursive data types based on terminals and their ancestries?

user_1243445 0
Viewed 142

Let's say I have a type that looks like this:

data Term a = Terminal a
| Application (Term a) (Term a)
| Abstraction String (Term a)

Now, I want to map Term a to Term b. Ideally, I would be able to do this using a function (a -> b) and just implement fmap. However, that doesn't work for me. The map from Terminal a to Terminal b is dependent not just on the value of a, but also the values of the ancestors of Terminal a (e.g. the depth of Terminal a). So it's more like [Term a] -> b which is messy, so I'm trying to decompose this into something cleaner.

So really, what I need is something like 2 functions and an initial value: (c -> Term a -> c) can be called on each of the ancestors in order to accumulate whatever we want. (I guess it's equivalent to ([Term a] -> c) but I'm not sure whether that confuses the situation or helps.) (c -> a -> b) can map Terminal a to Terminal b. (We also need an initial value of type c)

So I'm definition a function with the following type signature:

notQuiteANatTrans :: (c -> Term a -> c) -> (c -> a -> b) -> c -> Term a -> Term b

This isn't a natural transformation. (I don't think) Or if it is, it's mapping something like [Term a] -> [Term b] where each of those is the path from the root of the tree to the Terminal. Is there a name for this? Is there maybe a different way to decompose my arrows in order to get something cleaner?

functor functional-programming haskell
1 Answers

I'm not sure I entirely understand the problem, so apologies if the following goes off on an irrelevant tangent...

The map from Terminal a to Terminal b is dependent not just on the value of a, but also the values of the ancestors of Terminal a (e.g. the depth of Terminal a).

This sounds reminiscent of having to examine a tree to find, for example, its depth. For a tree, you can do this with its catamorphism - see e.g. the examples for foldTree.

In general, if you know the catamorphism for a datatype, you can derive most other (perhaps all?) useful functions from it. So what's the catamorphism for Term a?

F-Algebra

You can derive the catamorphism from F-Algebras. I'll follow the process I've used in my own article series on catamorphisms.

Define the underlying endofunctor like this:

data TermF a c =
    TerminalF a
  | ApplicationF c c
  | AbstractionF String c
  deriving (Eq, Show)

instance Functor (TermF a) where
  fmap _ (TerminalF a) = TerminalF a
  fmap f (ApplicationF x y) = ApplicationF (f x) (f y)
  fmap f (AbstractionF s x) = AbstractionF s (f x)

This enables you to figure out the catamorphism by using typed holes:

termF = cata alg
  where alg      (TerminalF x) = _
        alg (ApplicationF x y) = _
        alg (AbstractionF s c) = _

If you try to compile this sketch, the compiler will complain about the type holes and tell you what you need. I used this process to arrive at this function:

termF :: (a -> c) -> (c -> c -> c) -> (String -> c -> c) -> Fix (TermF a) -> c
termF t appl abst = cata alg
  where alg      (TerminalF x) = t x
        alg (ApplicationF x y) = appl x y
        alg (AbstractionF s x) = abst s x

The catamorphism requires a mapper of the underlying type a -> c, as well as 'accumulators' for each of the recursive nodes.

Isomorphism

Fix (TermF a) is isomorphic with Term a, as witnessed by these two conversion functions:

toTerm :: Fix (TermF a) -> Term a
toTerm = termF Terminal Application Abstraction

fromTerm :: Term a -> Fix (TermF a)
fromTerm = ana coalg
  where coalg      (Terminal x) = TerminalF x
        coalg (Application x y) = ApplicationF x y
        coalg (Abstraction s x) = AbstractionF s x

This means that you can easily define the catamorphism for Term a using the catamorphism for Fix (TermF a). Let's call it foldTerm, as that's probably a little more idiomatic:

foldTerm :: (a -> c) -> (c -> c -> c) -> (String -> c -> c) -> Term a -> c
foldTerm t appl abst = termF t appl abst . fromTerm

Now that you know the type of foldTerm, you can throw away all the TermF machinery and implement it directly.

Direct implementation

Again, you can use typed holes for a simpler, more direct implementation:

foldTerm :: (a -> c) -> (c -> c -> c) -> (String -> c -> c) -> Term a -> c
foldTerm t appl abst      (Terminal x) = _
foldTerm t appl abst (Application x y) = _
foldTerm t appl abst (Abstraction s x) = _

The compiler will tell you what you need, and it's fairly clear that the implementation must be something like this:

foldTerm :: (a -> c) -> (c -> c -> c) -> (String -> c -> c) -> Term a -> c
foldTerm t appl abst      (Terminal x) = t x
foldTerm t appl abst (Application x y) = appl (recurse x) (recurse y)
  where recurse = foldTerm t appl abst
foldTerm t appl abst (Abstraction s x) = abst s (foldTerm t appl abst x)

Keep in mind that the output of foldTerm can be any type c, including Term b: c ~ Term b. Does that enable you do do what you're asking about?

user_1260140
Related