Re: Parametrically polymorphic operations (Was: Safe C++)

[Brian Rogoff <bpr@shell5.ba.best.com>]

On Thu, 20 Sep 2001, Jacob Sparre Andersen wrote:
> Chad:
> > "Brian Rogoff" <bpr@shell5.ba.best.com> wrote in message
> [...]
> > > Parametrically polymorphic functions
>
> > I'll have to trust you or these three since I have never encountered a
> > situation where I was ever wishing for such functionality.
>
> While working on libraries for matrix operations and unit
> safe types, I have certainly wanted something very similar
> to parametrically polymorphic functions. It would make it
> possible to have more extensive compile time checks, than
> what is possible with Ada as it is defined today.
>
> An example:
>
>    type Matrix (Left, Right : Positive) is private;
>
>    function "*" (Left  : in Matrix;
>                  Right : in Matrix (Height => Left.Width))
>      return Matrix (Width  => Right.Width,
>                     Height => Left.Height);
>
> (I hope the intention is clear although the syntax isn't
> defined)

That you want to multiply an M x N and a N x K matrix and have it type
check at compile time and produce an M X K matrix?

I only very recently learned how to do this in ML (look for a posting by
Matthias Blume on comp.lang.ml replying to one of mine in the last year)
and I have to say it was a bit surprising. I guess it shouldn't have been;
one of the ideas in the technique is the same as used to create a type
safe printf library (printer combinators) and is just generally useful.
I don't know if it's really appropriate to post it here since it's a fair
bit (~200 lines) of non-Ada code :-).

> This would tell the compiler a few things, which would allow
> it to flag type mismatches already at compile time.

With the technique I mention, there is no question of the compiler being
"allowed" to flag the mismatch. The dimensions are moved into the type
system so the type checker rejects it! Just like with the printer
combinators.

-- Brian