Get term type during evaluation using Hindley-Milner type system

I've implemented a lambda calculus evaluator and use the Hindley-Milner algorithm to infer terms types and ensure type correctness without the user having to explicitly annotate types.

But now I'd like to add a typeof operator that given a term, it returns the type of the term. So far, what I do is keep a hash map of terms to types that is populated during type checking. So if I do typeof 123, when the type checker determines the type of 123, it'll add 123 = Number to the hash map and look it up when typeof 123 is evaluated.

The problem with this approach is that if I have this term:

let _typeof = \a.(typeof a) in (_typeof 123)

Since \a.(typeof a) is polymorphic and has type a -> Type, the result will be a instead of Number as I'd expect. If instead I had this:

(_typeof.(_typeof 123) \a.(typeof a))

Then I'd get the right type Number since \a.(typeof a) is not polymorphic.

So all I need is a way to handle polymorphism. I'm having a hard time getting my head around it and I wonder if there is a known way to do this.

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 -> preterm -> term

and an evaluator

eval : env -> term -> value

The evaluator now has an easy time evaluating typeof e as

let rec eval env = function
  ...
  | Typeof e -> 
    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 α -> 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 α -> 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.

StackExchange Computer Science Q#61184, answer score: 2