Re: Problem with type inference
Andre van Tonder 15 Sep 2005 20:03 UTC
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