Why Mathematical Soundness Matters.
haskell.vivian.mcphail at gmail.com
Sat Apr 21 00:33:01 EDT 2007
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.
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
> 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 _ _)
Another method is to manipulate the expressions as ASTs and convert to the
concrete using TH.
But what about dynamic data?
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).
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-prime