Would you be so kind as to elaborate?
Sure. I'll just sketch how to deal the example in your e-mail. If you want to use recursive data types (like Lists or Trees), you'll need to use the Expr data type from the paper. Instead of defining:
data Foo = One | Two | Three | Four
Define the following data types:
data One = One data Two = Two data Three = Three data Four = Four
You can define the following data type to assemble the pieces:
infixr 6 :+: data (a :+: b) = Inl a | Inr b
So, for example you could define:
type Odd = One :+: Three type Even = Two :+: Four type Foo = One :+: Two :+: Three :+: Four
To define functions modularly, it's a good idea to use Haskell's clasess to do some of the boring work for you. Here's another example:
class ToNumber a where toNumber :: a -> Int
instance ToNumber One where toNumber One = 1
(and similar instances for Two, Three, and Four) The key instance, however, is the following:
instance (ToNumber a, ToNumber b) => ToNumber (a :+: b) where toNumber (Inl a) = toNumber a toNumber (Inr b) = toNumber b
This instance explains how to build instances for Odd, Even, and Foo from the instances for One, Two, Three, and Four. An example ghci sessions might look like: *Main> let x = Inl One :: Odd *Main> toNumber x 1 *Main> let y = Inr (Inr (Inl Three) :: Foo *Main> toNumber y 3 Of course, writing all these injections (Inr (Inr (Inl ...))) gets dull quite quickly. The (<) class in the paper explains how to avoid this. I hope this gives you a better idea of how you might go about solving your problem. All the best, Wouter