Why Mathematical Soundness Matters.
Vivian McPhail
haskell.vivian.mcphail at gmail.com
Sat Apr 21 00:33:01 EDT 2007
Hi All,
This is in regard to previous posts about mathematical preludes.
> class Set a
>
> class (Set s) => SemiGroup s o where
> semigroup_op :: o -> (s,s) -> s
> -- closure
> -- associative
>
> class (SemiGroup s o) => Monoid s o where
> identity :: o -> s
>
> class (Monoid s o) => Group s o where
> inverse :: o -> s -> s
>
> class Optimisable a where
> cost :: Set b => a -> b
First, consider a semigroup, which is a set with an associative operation.
Into this structure falls Matrices with multiplication. There is scope for
optimisation of a series of multiplications. Inductively for each m1 * m2 *
m3 compare the cost of m1 * m2 versus m2 * m3 which can be simply obtained
from the size of the index of the matrix. Thus expressions like (14,3) x
(3,15) x (15,2) can be computed as (14,3) x ((3,15) x (15,2)) and not in a
more expensive way.
Furthermore, if we tag identities with a phantom type, we can eliminate
needless operations like 3 + 0.
Not as much optimisation can be achieved with inverses (3 + -3) because it
might be just as expensive to calculate that something is an inverse as to
do actual calculation.
So how can this optimisation be performed? Well this is a question that I
put forward to you, Gentle Reader.
Static:
It seems to me that expressions the types of which are known at compile-time
can be optimised by using type-level programming in combination with
compiler rewrite rules, e.g. if we have a type class SizeLarger then the
expression
> semigroup_op (semigroup_op m1 m2) m3
can be rewritten as
> semigroup_op m1 (semigroup_op m2 m3)
depending upon the SizeLarger types of the various (semigroup_op _ _)
function calls.
Another method is to manipulate the expressions as ASTs and convert to the
concrete using TH.
But what about dynamic data?
Dynamic:
These are terms whose types are not known until run-time (such as would
happen when loading an arbitrary matrix from a file). In this case we can't
use compiler term-rewriting or TH, but what options are there? Depending
upon the speed/complexity of type-checking versus computation would it not
be feasible to use run-time type checking (a polymorphic Dynamic type) to
achieve this optimisation? Yes there is a lot to said in favour of static
type-checking, but there are cases in which it is not feasible, witness
type-level bounds checking of run-time loaded matrices of unknown shape. In
a program that used run-time typechecking (yes there would be a
computational overhead) the dynamic stuff would be isolated from the
'trusted' statically checked program and values could only be injected
through trusted entry points (e.g. get4SquareDoubleMatrix :: Dynamic -> IO
(Array ((D4 $ Sz),(D4 $ Sz)) Double).
In any case, writing 'simple' arithmetic expressions would become more
cumbersome because of the overhead of annotating types and possibly moving
between ASTs and the concrete. But if we a had collection of mathematically
sound classes like SemiGroup, Monoid, Group, Field, etc... then these
optimisations could be built into the compiler and we could sugar the
programmer-side just as it has been for Monads.
In conclusion, I put this forward as a reason for Mathematically Meaningful
Numeric Classes and in obiter I am putting forward support for polymorphic
Dynamic types (run-time typechecking).
Cheers,
Vivian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20070421/fcf1cc1f/attachment.htm
More information about the Haskell-prime
mailing list