(This post is literate Haskell, available here.)

This post will show a trick for making it easier to work with terms representated as fixed-points of functors in Haskell. It is assumed that the reader is familiar with this representation.

First some extensions:

```
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
```

## Representing terms as fixed-points

A common generic term representation is as a fixed-point of a functor:

`newtype Term f = In { out :: f (Term f) }`

A simple example functor is the following, representing arithmetic expressions:

```
data Arith a
= Num Int
| Add a a
deriving (Functor)
```

One problem with the `Term`

representation is that it’s quite cumbersome to construct with it. For example, the following is the representation of the expression $(1+2)+3$:

```
term1 :: Term Arith
term1 =
In (Add
(In (Add
(In (Num 1))
(In (Num 2))
))
(In (Num 3))
)
```

This post will show a simple trick for inserting the `In`

constructors automatically, allowing us to write simply:

```
term2 :: Term Arith
term2 = deepIn10 $ Add (Add (Num 1) (Num 2)) (Num 3)
```

## Deep conversion of terms

First, let’s have a look at the type of the above expression:

`_ = Add (Add (Num 1) (Num 2)) (Num 3) :: Arith (Arith (Arith a))`

We see that the type has three levels of `Arith`

because the tree has depth three. So in general, we need a function with the following type scheme:

`f (f (f ... (f (Term f)))) -> Term f`

The purpose of this function is to insert an `In`

at each level, from bottom to top. The reason for having `Term f`

in the argument type (rather than just `a`

) is that `In`

expects an argument of type `Term f`

.

This function has to be overloaded on the argument type, so we put it in a type class:

```
class Smart f a
where
deepIn :: f a -> Term f
deepOut :: Term f -> f a
```

Here `f`

is the functor and `a`

can be `Term f`

, `f (Term f)`

, `f (f (Term f))`

, etc. The class also contains the inverse function `deepOut`

for reasons that will be explained later.

First we make the base instance for when we only have one level:

```
instance Smart f (Term f)
where
deepIn = In
deepOut = out
```

Next, we make a recusive instance for when there is more than one level:

```
instance (Smart f a, Functor f) => Smart f (f a)
where
deepIn = In . fmap deepIn
deepOut = fmap deepOut . out
```

And that’s it!

## Ambiguous types

Now there’s only one problem. If we try to use `deepIn $ Add (Add (Num 1) (Num 2)) (Num 3)`

, GHC will complain:

`No instance for (Smart Arith a0) arising from a use of ‘deepIn’`

As said earlier, the type of the given expression is `Arith (Arith (Arith a))`

, which means that we get an ambiguous type `a`

which means that it’s not possible to know which of the above instances to pick for this `a`

.

So we need to constrain the type before calling `deepIn`

. One idea might be to use a type function for constraining the `a`

. Unfortunately, as far as I know, it’s not possible to make a type function that maps e.g.

`Arith (Arith ... (Arith a))`

to

`Arith (Arith ... (Arith (Term Arith)))`

This is because `a`

is a polymorphic variable, and type functions cannot case split on whether or not a type is polymorphic.

But there is one thing we can do. The type `Arith (Arith (Arith a))`

shows that the expression has (at most) three levels. But there is nothing stopping us from adding more levels in the type.

Why not make a version of `deepIn10`

that forces 10 levels in the type?

```
type Iter10 f a = f (f (f (f (f (f (f (f (f (f a)))))))))
deepIn10 :: (Functor f, a ~ Iter10 f (Term f)) => f a -> Term f
deepIn10 = deepIn
```

This function can be used to insert `In`

constructors in terms of at most depth 10.

## Constructing terms from existing terms

The above example, `term2`

, was constructed from scratch. We might also want to construct terms that contain other, already constructed, terms. This is where `deepOut`

comes into play:

`term3 = deepIn10 $ Add (deepOut term2) (Num 4)`

## No comments:

## Post a Comment