Re: Problem with type inference

[Andre van Tonder <andre@xxxxxxxxxxxxxxxxx>]

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
                                         #f
                                         #f
                                         #f
                                         #f
                                         '((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))

or

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

Cheers
Andre