[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Problem with type inference

On Thu, 15 Sep 2005, William D Clinger wrote:

Andre van Tonder wrote:
> I would like to point out that, with a primitive procedural
> interface, static type inference becomes hard.
I would like to understand this argument.

I was thinking in terms of simple HM-like typing, where I just meant that in examples like

  (define make-x (record-constructor y))

the type of make-x cannot be inferred from what I naively understand as the HM type of y, but rather seems to depend on the evaluated y.

I understand that many record type definitions, such as

  (define y (make-record-type-descriptor 'point
                                         '((mutable x) (mutable y))))

can easily be analyzed at compile-time. But what should be a static type of y that incorporates the available information, what type can we assign to RECORD-CONSTRUCTOR that will extract this information to give the correct type for MAKE-X above, and what if we had as the last argument the expression

  (list '(mutable x) '(mutable y))


  (f '(mutable x) '(mutable y))

where f :: List ->  List.

In other words, is the basic interface compatible with static typing a la HM?

It seems that whatever format the static inferencer expects, the programmer can easily shoot himself in the foot and break all inferencing in implementing a custom syntactic layer that perhaps translates to a slightly different format.

I concede that this will not matter if the programmer uses the standard syntactic layer.