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