On Wed, Oct 21, 1998 11:30 Uhr, Ch. A. Herrmann
<mailto:[EMAIL PROTECTED]> cheered about my unboiled ideas:
> >> instance Commutative (==) instance Commutative (+) :: Int -> Int
>
>The type is important here. Properties sometimes are not compatible with
>the class hierarchy.
This would go with haskell's ability to restrict overloaded (polymorphic)
functions to specific types. Since computers are not able to faithfully
mirror mathematics, the laws of math will break down in certain places as
you say. The most obvious that comes into my mind is the broken
associativity of limited precision float multiplication:
> property Associative a where
> a x (a y) = a (a x) y
>
> instance Associative (*) :: Float -> Float
would be a lie to the compiler, but in certain cases, where precision is
not the main objective, it could lead to quite good performance.
Associativity is recovered when moving down the class hierarchy from Number
to Integral.
What I was thinking of was a pragma-like mechanism for aiding the compiler
to perform transformations, that without these guides would not be
possible. Where the compiler is able to infer the properties by itself, the
pragmas would be redundant, but could still be a kind of documentation.
Where the pragmas (= property instance declarations) would conflict with
the inferred or ground properties, a warning could be issued (such as in
the above case). If the compiler cannot infer the property by itself (where
are the current limits?), then it could use the declaration or ignore it.
OTOH one cleverly set declaration could kick off an avalanche of inferences
in succession.
> >> instance Isomorhism (f, g) where
> >> f x = (+x)
> >> g x = (+(-x))
>
> Gabor> Of course in both where clauses "x" must stand for the same
> Gabor> object.
>
>I don't understand what you mean. Both occurrences of "x" are bound
>by the function definition and are therefore not visible outside.
>
Yes, what I meant was that x has to stand for the same variable in the two
where-clauses. Otherwise, one would end up with (+5) =iso= (+(-7)) which is
of course not the case. This would be contrary to the haskell convention,
where each definition introduces its own variables and they are independent
despite of a possibly identical name. The above is more than with logical
languages, with x being a logical variable. This would be the case for the
(top-level) variables introduced by the left hand sides, or explicit
variable declarations in a distinct where-clause, like in this contrived
example:
> instance Isomorphism (f, g) where
> x :: Integer
> f = \ a => a + x
> g = \ a => a - x
Here the variable "a" should not be the same across where-clauses, but "x".
In the meantime I thought of another useful application of properties:
> property Disjoint (f, g) :: (a -> Bool, a -> Bool) where
> f x ~= g x
This way one could state the trichotomy of integers:
> instance Disjoint ((<y),(==y)) :: (Int -> Bool, Int -> Bool)
> instance Disjoint ((>y),(==y)) :: (Int -> Bool, Int -> Bool)
The third instance should be inferrable (by the definition of (<)):
> instance Disjoint ((<y),(>y)) :: (Int -> Bool, Int -> Bool)
Hope this leads the thoughts further...
Gabor
