# [racket] Historical note on type inference

 From: Hendrik Boom (hendrik at topoi.pooq.com) Date: Wed Aug 6 07:49:58 EDT 2014 Previous message: [racket] Puzzled about type inference Next message: [racket] Puzzled about type inference Messages sorted by: [date] [thread] [subject] [author]

```On Tue, Aug 05, 2014 at 11:00:47PM +0100, Norman Gray wrote:
>
> Alexander, hello.
>
> On 2014 Aug 5, at 14:11, "Alexander D. Knauth" <alexander at knauth.org> wrote:
>
> > Well ann can’t add any detail, it can only make types less specific.
>
> Aha: I was thinking of this the wrong way round.
>
> If I type, say, #(1 2) into TR, it determines its type as
>
> > #(1 2)
> - : (Vector Integer Integer)
> '#(1 2)
>
> Compared to that,
>
> > (ann #(1 2) (Vectorof Positive-Integer))
> - : (Vectorof Positive-Integer)
> '#(1 2)
>
> ...is more specific.  But your explanation makes me realise that the most specific possible type is (Vector 1 2) (of limited utility), and that (Vector (U 1 2) (U 1 2), (Vector Integer Integer) and (Vectorof Positive-Integer) are just samples of the many possible less specific ones, and it happens that the less-specific one that TR guesses I want is not the one I actually want.  Which is why I have to use `ann`.

I first encountered this type-ambiguity with Algol 68, long long ago.
But in that language, the type affected physical data representation,
so it was necessary to deal with it quite explicitly.

When, analogously, you have a choice of turning (1, 2.0) into
either array of (union of integer and real) or array of real, it really
matters which to choose.  For Algol 68, the resolution of these kinds
of quandary was actually specified in the (not context-free) grammar,
and it practically never went wrong.  The cases that seemed ambiguous
to humans were mostly blocked syntactically and had to be resolved
explicitly with casts.

Indeed, much of the complexity of its language definition was involved
with resolving the interactions between various degrees of contextual