Hi,
I spend a lot of time developing a generic C++ library to handle
symbolic manipulation of (nearly) arbitarily polynomials. There are a
lot of cases when (the so called) type system of C++ is no of help and
I needed to implement my own kind of dynamic types with checking at
runtime. For example let K be a field and let A and B be two
Polynomials. At runtime we set up variables x and y , then construct
two different polynomial Rings K[x] and K[y] and then state that A is
an element of K[x] and B is an element of K[y]. Now A and B may share
the same structure in the data structures that represents them and
both are univariate polynomials but the expression A = A+B is
senseless and invalid. This is a case that no static type checker can
detect, so don't expect to much from it (and don't expect anything
usefull from the stupid implementation of templates in C++). This and
several others made me exploring some functional languages to
reimplement a enhanced version of my library. Up to now it appears to
me that I still have to code some of the type-checking by hand,
because anything else seems to require a complicated theorem prover at
compile time.
ciao Juergen
Herbert Graeber wrote:
> I have taken a look on these papers at
>
> http://www.cl.cam.ac.uk/~ajk13/
> http://ftp.cs.chalmers.se/users/pub/rittri/dimpolyrec.ps.Z
>
> But I discovered, that there is one important difference to the C++ example
> I posted. The type system is extended to allow inference of deimensions. The
> C++ version does not need extensions specific to dimensions. The language
> features already present (templates) allow this without extending the
> language.
>
> I think there is no way to add compile time dimension checking (and many
> other similar things) in Haskell. May be Haskell 2 should contain an
> extended type system, that allows that. I am not firm with depended types.
> Perhaps that's the way do such things.
>
> Cheers,
> Herbert
