Get term type during evaluation using Hindley-Milner type system
Hashing of terms to types sounds like a hack to me (or possibly premature optimization and a hell created by stateful programming). During type inference you should tag every subterm with its computed type. Then during evaluation typeof simply projects the type.

The hell is in the deatils, of course. Here are some initial thoughts about how this would go (I did not actually implement this, but if I did, I would start from Poly in PLZoo).

We define the following datatypes:


a datatype ty of polymoprhic types
a datatype preterm of raw terms (the parser gives you these)
a datatype term of tyepchecked terms (type inference converts preterms to these)
a datatype value of values


Maybe like this, using OCaml syntax:

(* the result of parsing is a preterm *)
type preterm =
  | PreType
  | PreNumeral of int
  | PreTypeof of preterm
  | PreVar of string
  | PreLet of string * preterm * preterm
  | PreApp of preterm * preterm
  | PreLambda of string * preterm

type ty =
  | Type (* the type of all types *)
  | Number
  | Parameter of int
  | Arrow of ty * ty

(* after type inference every term is tagged with its type *)
type term = term' * ty
and term' =
  | Type
  | Numeral of int
  | Typeof of term
  | Var of int (* using de Bruijn indices *)
  | Let of term * term (* using de Bruijn indices *)
  | App of term * term
  | Lambda of term (* using de Bruijn indices *)

(* a typing context *)
type ctx = ty list

(* a runtime environment *)
type env = value list

(* values are explicitly tagged with their types *)
and value = value' * ty
and value' =
  | ValType of ty
  | ValNumeral of int
  | ValLambda of env * term


The parser gives us a preterm. Then we define

infer : ctx -&gt; preterm -&gt; term


and an evaluator

eval : env -&gt; term -&gt; value


The evaluator now has an easy time evaluating typeof e as

let rec eval env = function
  ...
  | Typeof e -&gt; 
    let (_, t) = eval env e in
      (ValType t, Type)
  ...


Let us work through your example

let _typeof = (λ x . typeof x) in _typeof 123


First, infer would find out that _typeof has type α -&gt; Type. In the application _typeof 123 it would try to match (a fresh instance of) α against the type Number and would succeed with setting α = Number. It would then conclude that the type of _typeof 123 is Type.

Second, when eval gets to evaluation of _typeof 123 it actually sees something like

(App ((Var 0, Arrow (Parameter 0, Type)), (Numeral 123, Number)), Type)


which is an application of bound variable 0 to the numeral 123, together with typing information: the bound variable 0 has type Arrow (Parameter 0, Type) which corresponds to α -&gt; Type, the numeral has type Number, and the entire expression has type Type. The evaluator first evaluates

(Var 0, Arrow (Parameter 0, Type))


which involves looking up the 0-th variable in the environment. It gets back a pair ((env', e), Arrow (Parameter 0, Type)) where (env', e) is a closure representing λ x . typeof x. Then it evaluates the argument and gets (ValNumeral 123, Number). It remains to evaluate e applied to (ValNumeral 123, Number) which is done the usual way with a recursive call to eval in env' extended with (ValNumeral 123, Number). Here e is going to be something like

(Typeof (Var 0, Parameter 0), Type)


which corresponds to the expression typeof x, except that x is replaced by de Bruijn index 0 and is tagged to have "any type". Now we need to pay attention (here is where you have a mistake that gives you α instead of Number): we first evaluate (Var 0, Parameter 0) by looking up the 0-th elemenent of (ValNumeral 123, Number) :: env', so we get (ValNumeral 123, Number). Now we evaluate Typeof by taking the second component, which is Number. It would be wrong to evaluate Typeof by simply returning Parameter 0, we actually have to evaluate its argument and then take the type of that). The final value therefore is

(Type Number, Type)


as expected.