[racket] Historical note on type inference

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 
strength and operator everloading.  The interaction between upward and 
downward moving type information was termed "coercion".

-- hendrik