Hi Y'all,
please ignore this message if you have the impression that I am writing
complete nonsense :-)
I am wondering if it would be feasible to declare laws that are guaranteed
to hold for some objects in a Haskell-like functional language.
For example I would like to declare that (+) is commutative. This would
have the benefit, that the compiler could optimize the parameter passing to
a commutative function by not having to swap arguments on the stack:
> is5 x = x == 5
could transform to
> is5 x = 5 == x
thus improving machine code from
pop x
push 5
push x
jmp (==)
to:
push 5
jmp (==)
even when (==) was no builtin primitive.
A convenient (Haskellish) syntax I could come up with is:
> property Commutative f where
> f a b = f b a
>
> instance Commutative (==)
> instance Commutative (+) :: Int -> Int
And stating a relation between two objects:
> property Isomorhism (i, j) where
> i . j = id
> j . i = id
>
> instance Isomorhism ((+x), (+(-x)))
here the last line would be the abbreviated version of
> instance Isomorhism (f, g) where
> f x = (+x)
> g x = (+(-x))
Of course in both where clauses "x" must stand for the same object.
Otherwise no connection could be established between f and g.
Writing down the relation in one line as an equation seems impossible to me
since f has to be defined independently from g. The instance declaration
simply
establishes the connection.
Now a more difficult example:
> property NaturalTransformation n where
> Functor f
> Functor g
> mor :: a -> b
> n . (f::map) mor = (g::map) mor . n
Here "(f::map) mor" stands for the the lifted morphism with respect to f.
Now state that reverse is natural:
> instance NaturalTransformation reverse
It should be possible to infer that both functors f, g are the list functor
[].
Does this all make sense? Is there another mechanism that already
accomplishes this?
Bye,
Gabor
