[Types-sig] recursive types, type safety, and flow analysis

[Greg Stein]

On Wed, 22 Dec 1999, Paul Prescod wrote:
> Greg Stein wrote:
> > "Means"? Not at all. I'm only suggesting we watch what happens with the
> > types. We have to do that *anyhow* to do the type checking.
> 
> I say: "given the name of the thing and the type associated with the
> name, we check that the operations are legal." Seems straightforward.
> We've been doing it since the 60's.
> 
> You say: "given the name of the thing we will intuit a type (often an
> anonymous/union type (which I consider confusing)) and then check that
> the operations are legal." 

That's not what I've been saying. I take blame for not making myself
clearer in this case.

> "Classic" type inference works from the operators to figure out what the
> types are. "Classic" type checking works from the names to validate the
> operators. You want both. I don't think that it will work in practice.
> The will be the semantics will be confusing as hell and the error
> messages will be totally indecipherable.
> 
> I am willing to iteratively open up the design to types of type
> inferencing and discovery as time goes by but I don't yet understand
> your model well enough to be able to write a specification around it.

Given:

  x = a + b

I don't want to infer anything from the "+" there. So no... this wouldn't
be called "classic type inferencing." John Skaller best described it as
type deduction. I want to know the type of x, given the types of a and b.

1) In the above statement, we already know the types of "a" and "b" (if
   not, then they haven't been assigned to and we can raise an error!).
2) We know what the "+" operator does, given those two types.
3) We produce a result type.
4) We associate that result type with "x".

In your model, (4) is replaced by "validate the result type against the
declared type of 'x'".

Otherwise, there is no difference between our proposals.

Your statements about not working in practice, confusing semantics, and
indecipherable error messages are simply FUD. You said yourself you were
unsure of the model that I was proposed. And FUD like this generally
peeves me.

I'm talking about figuring out types from the assignments, not from
declarations. That's it. Forget declarations and the clutter that they
bring to programs.

-g

-- 
Greg Stein, http://www.lyra.org/