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

Re: Problem with type inference

This page is part of the web mail archives of SRFI 76 from before July 7th, 2015. The new archives for SRFI 76 contain all messages, not just those from before July 7th, 2015.

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.