On Wed, Oct 21, 1998 10:10 Uhr, Johannes Waldmann
<mailto:[EMAIL PROTECTED]> wrote:
>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).
The properties of single or interrelated objects are only relevant in the
optimizer phase, and I guess that here a mechanism is already in place to
prevent infinite loops of rewrite operations.
>
>> > 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.
>
What if the function type is not sufficiently polymorphic, thus the free
theorems do not apply? It would still be useful to declare naturality for a
non-polymorphic function.
>naturality here allows for shifting of cata/holymorphisms
>(aka deforestation) which is already implemented in ghc?
>
I guess so, though I strongly suggest leaving holymorphisms to be dealt by
the gods! :-)
Gabor
