[Haskell-cafe] Data.Generics question

[Carl Witty]

On Tue, 2006-12-19 at 09:25 -0500, Mark T.B. Carroll wrote:
> Hmmm. That's interesting. I have a slightly different problem and I
> don't know if it's relevant or not. I have nested algebraic data types
> for things like expressions with terms and operators and whatever too,
> and some of my functions do a transformation that removes all instances
> of particular constructors (by expressing them in other ways) but that
> leaves most of the data structure intact. I'd love to use the type
> system to enforce the constraint that the result from the transformer
> function has eliminated occurrences of certain constructors within the
> nested type, but to do that I seem to have to create a whole other
> near-copy of the data declarations with slightly different names and the
> occasional constructor missing. I wonder if there's a better way.

I think you may be able to do this with OOHaskell (but I've never used
OOHaskell, only read the paper, so I'm not positive).

Extensions to the type system like regular expression types, as featured
in OCamlDuce (and, afaik, all the *Duce languages) make this
straightforward, but are probably overkill for this application.  (And
extending Haskell with regular expression types strikes me as extremely
difficult, unless you follow the OCamlDuce example where regular
expression types are their own separate world and don't interact with
polymorphism.)

I have another, lower-tech solution: 

Warning: I haven't actually written much Haskell code in a long time,
and I don't have time to test this, so it may use bad syntax.

Suppose you have the type:

> data Expr = Plus Expr Expr | Minus Expr Expr | Base Int

And you have a normalize function that gets rid of "Minus" constructors.
For a version of the data type that can check that normalize does, in
fact, eliminate all Minus constructors, you can do this:

> data Expr' m = Plus (Expr' m) (Expr' m) | Minus m (Expr' m) (Expr' m) 
>   | Base Int

Then "Expr' ()" is isomorphic to the original Expr type (if you ignore
the possibility of bottom values), and

> -- GHC extension: data type with no constructor
> data Void

"Expr' Void" does not allow Minus constructors (again, ignoring the
possibility of (undefined :: Void)).

So you can give normalize the type:

> normalize :: Expr' () -> Expr' Void

If you don't want to use the GHC extension, the following type signature
has the same effect:

> normalize :: Expr' () -> Expr' a

I'm not sure how useful this approach is in practice.  If you have many
compiler phases, each of which allows a slightly different set of
constructors, then you may need many type parameters to your types.
(Although to a certain extent this can be hidden with type aliases.)
Also, you need to worry about the witnesses in all your pattern-matching
code, which is annoying.

Carl Witty