Gabor Greif writes on defining properties,
to make program transformation for the compiler easier.
it might generally be a good idea to have some syntax
to describe assertions (in a very general sense) -
i think Eiffel folks could tell us how to do this properly.
i'd like to see answers to Gabor's first example (commutativity).
on a general note, this leads to term rewriting
modulo some equivalence relation (comm. and assoc. seem most common),
which gets pretty tough (all your basic tools: unification,
confluence, termination, get considerably more complicated).
it's even harder than that (since functional programs are higher order terms).
> > property NaturalTransformation n where
> > n . (f::map) mor = (g::map) mor . n
> > instance NaturalTransformation reverse
however the compiler knows this, from the type of reverse :: [a] -> [a].
what you're stating is the "free theorem" for that type.
naturality here allows for shifting of cata/holymorphisms
(aka deforestation) which is already implemented in ghc?
--
Dr. Johannes Waldmann Institut fur Informatik Universitat Leipzig
[EMAIL PROTECTED] http://www.informatik.uni-leipzig.de/~joe/
Augustusplatz, D-04109 Leipzig, Germany, Tel/Fax (+49) 341 97 32 204/209
