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