"Compile-time" patterns

If I define a function like

f[x : {_, _Integer}] := (* function body *)


then, as I understand it, every time f[expr] is encountered during the evaluation, expr will be matched against {_, _Integer} to determine which definition for f (if any) should be used.

Has anyone tried to implement "compile-time" patterns in mathematica, which would select definitions before evaluation? For example, if I had some code like

(* ... *)
a = {"ok", 24};
(* ... *)
f[a];


and I had certain extra constraints on how a was used in that code, determined what could "touch" its definition and how it got modified at those times, etc., I might be able to determine that I should always use the f[x : {_, _Integer}] definition of f before I even started evaluating.

If it turns out patterns per se are too flexible for this, I wonder if one could define explicit "type declarations" to implement the same behavior; for example, the definition for f might look like

f[x ::: {_, _Integer}] := (* body *)


and all declarations and modifications of a that I expect to use in my calls to f might come with some type declaration, like

a = {"ok", 24} ::: {_, _Integer}


I'm using the pattern {_, _Integer} just as before here, but maybe only some restricted subset of patterns would be feasible to use here to ensure termination (or such)—for example, perhaps a complicated pattern like {_, _?f} where f is an arbitrary predicate would be disallowed for these kinds of declarations.

Then, for an expression that involved these kinds of type declarations to evaluate, we would need to be able to check the times any definition was modified, and be able to see by way of these declarations that the declaration was preserved. For example, if I had the syntax a = {"ok", b} ::: {_, _Integer}; in my expression, I would also need to be able to prove that I could infer b ::: _Integer from this expression or from the context.

Certain "dangerous" operations, like ToExpression["a = 2"], spring to mind as potential obstructions. These might also need to be weeded out, and if safety is our goal, perhaps only a subset of the Wolfram language would be usable in the evaluation of expressions containing type declarations. (Otherwise, perhaps a warning message could simply be printed whenever a type-dangerous operation was performed in a way that might interfere with the type declarations.)

When I have some time, I'd maybe like to try to build this; but in the meantime, I was wondering if anyone had seen anything like it done for the Wolfram language already, or if they could see any big potential problems that I might be missing—or if I'm misunderstanding the way evaluation proceeds in a way that makes this unnecessary! (For all I know, maybe Mathematica already does this to the extent it can.)

• You can declare ""types" by giving them a special head. and defining operators for this type. Mar 12, 2021 at 16:11
• I’ve written a small package for this before, but I don’t think that addresses the “compile-time” issue, since (as I understand it) it checks to make sure the type constraints given by /; are not violated each time it evaluates the expression. Unless that’s not quite what you mean? Mar 12, 2021 at 23:57
• No. You can declare a custom type,e.g. myType[..] and give data and functions as arguments. And then you must eventually declare functions of this type. Mar 13, 2021 at 8:14
• That's what I'm referring to, which I've already done. How does this address the "compile-time" issue...? Mar 14, 2021 at 22:13
• myType is like an Object in object oriented programming. Mar 15, 2021 at 8:18