How to enforce/specify the type of a module local variables similar to the module arguments?

Question

In Mathematica, one can specify the type of a module argument by giving the Head name. I am using type loosely here since Mathematica does not have types. But this does basically the same thing. So when someone calls foo with argument which is not an integer, and foo is defined to accept an argument whose head is integer, the call will not go through.

This is all great. But I'd like to do the same for local module variables. i.e. define a local variable that can only be assigned say Real values or only Integer values. But I can't do this now.

The question is, is there a way to do this?

I will give an example below how this is done in Maple, and how to do the same in Mathematica if possible. Here is a simple function that accepts only an integer. It then defines a local variable of type float which maps to Real in Mathematica. When it tries to assign an integer value to this variable, this is caught at run time by Maple and it gives an error. I find this feature very useful, and use it all the time, as it helps in finding errors in my code and I find it makes the code more robust.

restart;
interface(warnlevel=4);
kernelopts('assertlevel'=2):
foo:=proc(n::integer)
local m::float:=0.0;
m:=n;
end proc;

And now

foo(1)

Here is the Mathematica translation. I could only enforce the type on the arguments, but do not know how to do it for the local module variable.

ClearAll[foo]
foo[n_Integer]:=Module[{m=0.0},
m=n
]

And now

foo[1]
(*1*)

Does there exist any methods in Mathematica to do the same as in the Maple example? I understand again that Mathematica does not have types like Maple, but may be there is other workaround to emulate this?

V 13.1 on windows

Answer 1

The code below might work.

As an example of the usage of the function type below, for a variable s,

type[s,Real];
s=4

sends an error message.

First we define the error message :

type::type = " `1` does not have type `2`" 

the second type in the syntax above is a tag name that I chose for the error message, 1 and 2 will refer to the arguments of the function type. Specifically, 1 refers to the variable and 2 refers to the type such as Real.

Next we define the function:

type[var_, $type_] :=
var /: HoldPattern[Set[var, Except[_$type]]] := (
    Message[type::type, HoldForm[var], $type]; Abort[]);

In words : type sets an UpValue or "property" to var such that it sends an error message whenever it appears in an assignment where the right hand side has the wrong type and then aborts. The HoldForm is used in the event that the variable was already assigned another value before.

Test:

Clear[c];
type[c, Real];

c = 3

c = 4.2

(* 4.2 *)

Next we use that in a module:

f[s_] :=
 Module[{int, real, graph},
  type[int, Integer];
  type[real, Real];
  type[graph, Graph];
  graph = x;
  (*real=4*)
  int = Pi;
  ]

One may comment and un-comment various assignments in the code above but it seems to work in all cases I checked.

Note: I did not use Clear in the definition for type so if the variable was assigned a value with the right type then later the wrong type, it will keep its previous value with the right type. That may or may not be desirable and one may or may not want to include a Clear in the function type.