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