**Problem Detail:**

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.

###### Asked By : Juan

#### Answered By : Andrej Bauer

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.

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/61184

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback