# 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.

• Thanks for the detailed answer. Just to make sure I understand, would this imply replacing type variables with types taken from the environment during evaluation every time polymorphic terms are evaluated, even in places I'm not calling typeof so that types are propagated until I eventually call typeof?. So for instance (λa.λb.a 123)should return a value & type tuple, and the type be b -> Number which would be the result of replacing the type a with Number during evaluation. – Juan Aug 4 '16 at 7:17
• Please do not use the same letter for the variable and for its type, that is a great source of errors. So instead of saying that λ a . a has type a → a you should say that that λ x . x has type α → α. For instance, you say "replace the type a with Number during evaluation", but in the expression λ a . λ b . a 123 the symbol a is not a type, it is an argument. And note that you did not use b at all. – Andrej Bauer Aug 4 '16 at 9:49
• I think λ x . λ y. x 123 should have type (Number → α) → (β → γ) → α. Did you mean to write λ x . x 123? – Andrej Bauer Aug 4 '16 at 9:51
• Maybe you think that since we're going to evaluate everything to tuples (value, type) all λ-abstractions will take two arguments? That is wrong. The type annotations are "hidden in the background" (the evaluator "secretly" keeps track of types). The identity function is still written as λ x . x and not as λ x . λ a . x. – Andrej Bauer Aug 4 '16 at 9:54
• That was really just an example. I meant to say, since λa.λb.a has type α → β → α, applying this to 123 during evaluation should return the value λb.123, which has type β → Number, and this type would need to be constructed during evaluation (in the background as you said) each time the function λa.λb.a is called by basically cloning the type of λb.a which is β → α and replacing every occurrence of α (or its de Bruijn index) with Number to get β → Number. – Juan Aug 4 '16 at 10:23

You may want to consider the approach Haskell uses to solve this problem, which is to say via typeclasses. A typeclass is a set of functions that can be implemented by many types. When a polymorphic function needs to be able to call such a function on a type that is unknown, it is silently modified to add an extra parameter, the "dictionary" for the type's instance of the type class (which is a structure containing the functions for that type's instance). Then call sites where the actual type is known are silently modified to pass the correct instance, and so on.

Then you just need a type class "Typeable" that is automatically defined for all types and which contains an appropriate "typeOf" for each defined type.

This may not be the easiest way of achieving what you want, but it leaves you with extremely useful general mechanism for solving many kinds of polymorphism problems, so it might be the most useful way of achieving what you want.

Simplifying the way this works in Haskell slightly (because AIUI Haskell's implementation involves an optimization that is conceptually unnecessary):

The typeclass Typeable is translated to a record type containing a function forall a . a -> Type. The function typeOf is defined with type Typeable a => a -> Type which means that there is an implicit parameter of type Typeable. typeOf is defined to simply unwrap the function from the record and call it.

A polymorphic function that calls typeOf needs to get a dictionary for its type argument, so any such function is inferred to have type Typeable a => [whatever the type would have been originally] for any type variable a that it needs to call typeOf for. This also means that there is an implicit argument to this function, too.

A function that calls typeOf for a known type has to provide an argument for the implicit arguments. This is calculated during the type checking phase, and it picks an appropriate predefined instance for the type of the term (which it obviously knows, because it has just type-checked it).

So in your example from the comments, the type checker knows that the term typeOf is applied to has type [Number] so it picks an instance for that type and adds that as a parameter.

So far, this is just the usual implementation of typeclasses. The twist here is that the type checker treats Typeable as a special case and generates the instances itself on demand so there will always be an instance available for any type that exists in the program.

It may also be worth noting that the instance for [a] can potentially delegate to the instance for a and wrap/otherwise modify the result. This may reduce the number of instances that are required.

• Any clue of how's that implemented? I see that evaluating typeOf (if True then [] else [10]) will return the right type [Integer] even though the list is empty, so somehow the empty list "knows" is an empty list of integers without having to look into any of its items. – Juan Aug 2 '16 at 21:38