1
To my Proposal for the definition domain extension
in Haskell language
>>To separate a sublanguage of Haskell given by the corresponding
>>compilation key (say, -domExt ) or, maybe, by the compiler pragma.
>>[..]
>>This sublanguage allows the compiler to replace any function f with
>>the function f' being the extension for f.
>>[..]
Bjorn Lisper <[EMAIL PROTECTED]> writes
> This was discussed on the list a while ago, right? I remember Arvind arguing
> for this kind of transformation. I also think there is a need for it, or
> rather for a way to more in general tell the compiler that it is OK to use
> "almost correct" transformations, which need not be just extending the
> domain of a function. An example is to let the compiler consider addition of
> floating-point numbers to be associative (which it really is not, just
> approximately), which makes it possible to parallelise folds over it. This
> transformation can be very important in HPC applications, but its
> application requires the knowledge that the numerics doesn't go wrong.
>
> An interesting question is how to specify these kinds of transformations for
> the compiler in a flexible way.
It was discussed, to some extent. I just return to the subject.
The thing is rather important.
In my Proposal, a function extension may be caused by various reasons.
One of the reasons is _equations_ - bi-directed _rules_.
But the extension may be derived from other considerations as well.
The mode -domExt has to denote that any of such extensions is allowed.
Your example with the Float associativity, it also can be expressed via
the _equations_
(F) x*(y*z) :: Float === (x*y)*z :: Float
Right?
I also vote for bringing their denotations to the language.
Only - under some special compilation key - "non-logically" minded
users should not suffer from this innovation.
My proposal contains
Example 2. x - x :: Integer === 0 :: Integer
In both cases the equation (rule) specifications
(without any condition part - for the simplicity) may lead to the
impicit definition domain extension for the functions. The programmer
orders the compiler to consider the extended equivalence. This may
lead to the map extension.
I think this is useful. The correctness and the usage of the code
obtained in this way are on the user.
Only the _equations_ have to be more generic than {-# rules #-} in
GHC. They define the equivalence relation and can, in principle, be
applied in both directions. Also there are equations derived
automatically from the given equations, they also have right to
apply.
In the case of x - x :: Integer, the source of extension is the
possibility x = undefined.
The Float associativity (F) has the same source of extension.
But I fear, (F) presumes also more dangerous transformation.
The Float value may overflow mantissa (right?) and break the
associativity law. In this case, we rather have the change of the map
than the map extension. This also may be useful, because the result
remains correct at some subset of the argument domain.
(maybe, this means narrowing of a map?)
But there are other cases: the function extensions that are not
caused by explicitly given equations.
Example 1 of Proposal:
take' n xs = case (compare n 0, xs) of
(EQ, _ ) -> []
(GT, x:ys) -> x:(take' (n-1) ys)
(GT, _ ) -> error "...too short list"
_ -> error "...negative n"
take'' n xs = case (compare n 0, xs) of
(GT, x:ys) -> x:(take'' (n-1) ys)
_ -> []
Here -domExt gives the compiler principal possibility to replace
take' to take''.
According to which `rules' or to which other means there might
happen or not happen such a replacement, this is another matter.
> An interesting question is how to specify these kinds of
> transformations for the compiler in a flexible way.
I suggest the two tools.
1. -domExt
to allow the principal possibility to do the function extensions
2. {-# equations #-}
may work only under the -domExt mode.
The bi-directed rules, with the denotations for the strategy of
their application. The strategy may be
"apply like Rules of GHC",
"apply according to this ordering on expressions",
or maybe, something else.
To my mind, this is generic enough.
And _equations_, they do the example with the Float associativity
too.
But the details have to be elaborated.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
