Why Mathematical Soundness Matters.

[Vivian McPhail]

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