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