naive unit checking via strong typing and operator overloading

Viewed 123

I was reading about strong typing in Ada focused on units checking, and decided to test the naive approach out myself:

procedure Example is
  type Meters is new Float;
  type Meters_Squared is new Float; 
  function "*" (Left, Right : Meters) return Meters_Squared is
  begin
    return Meters_Squared(Float(Left)*Float(Right));
  end;
  len_a : Meters := 10.0;
  len_b : Meters := 15.0;
  surface : Meters_Squared;
  len_sum : Meters;
begin
  len_sum := len_a + len_b; -- ok
  surface := len_a * len_b; -- ok
  len_sum := len_a * len_b; -- invalid
end Example;

Now I know that this is not actually practical approach, I'm trying this just as a learning experience. And based on my attempts so far, I must be missing something, because when I try to compile the example listed above, I get no errors:

$ make example
gcc -c example.adb
gnatmake example.adb
gnatbind -x example.ali
gnatlink example.ali

While when I drop the function definition overloading the multiplication operator, it fails as expected:

$ make example
gcc -c example.adb
example.adb:14:20: expected type "Meters_Squared" defined at line 3
example.adb:14:20: found type "Meters" defined at line 2
make: *** [Makefile:6: example] Error 1

With this in mind, I don't understand how, with the multiplication operator overloading, the compiler could be ok with surface := len_a * len_b and len_sum := len_a * len_b at the same time.

1 Answers

Your "*" overloading is just that; Meters inherits

function "*" (Left, Right: Meters) return Meters;

from Float.

What you can do is suppress that inherited function:

function "*" (Left, Right: Meters) return Meters
is abstract;

In this case, marking the undesired function abstract removes it from consideration for overload resolution: in ARM 6.4(8) we have

... The name or prefix shall not resolve to denote an abstract subprogram unless it is also a dispatching subprogram.

and Meters isn’t a tagged type, so "*" isn’t dispatching.

You can also declare a non-overloaded subprogram abstract:

function "and" (Left, Right : Meters) return Meters
is abstract;

to which GNAT says cannot call abstract subprogram "and", because of ARM 3.9.3(7).

Related