brownplt / pyret-lang

The Pyret language.
Other
1.07k stars 110 forks source link

`Any` being abused to also mean "not yet defined" #1188

Open shriram opened 7 years ago

shriram commented 7 years ago

A bit like using 0 to mean both a legitimate value and an error, we're abusing Any to mean both itself and "this thing has not yet been ascribed a type". Can we instead:

  1. Add a meaningful type name like Not-Yet-Implemented and ascribe that to all the placeholders?

  2. Change the type error UI to notice that type and give a meaningful error, requesting that they contact us and let us know what they need?, and

  3. Add this to the logging interface so we can get rid of the "contact us" part?

Each of these can be done before the other so we don't have to block on all parts before we can stop issuing confusing Any errors…

blerner commented 7 years ago

My only engineering requirement on this is that we not add a new variant to the Type data-definition. If we build some vacuous data type: data NYI: end that we could detect easily, that would be a fine solution to (1) above.

shriram commented 7 years ago

Just for the record, can you summarize the reason for your requirement? It feels to me much cleaner that this be built into the data definition than hidden as a user-defined type (with hygiene issues, having to track where it was introduced into the code, etc.).

blerner commented 7 years ago

"We haven't finished implementing" isn't a feature of a type system. It should not require support in the type inference system, the type or annotation checking systems, etc. It shouldn't be a permanent feature that w have to give formal semantics to. It should solely be in the provence of error message reporting.

shriram commented 7 years ago

Actually, the Typed Racket (and every other retrofitted type system) experience implies that it will always be a feature of the type system. This is the type that says, essentially, "the language has gotten ahead of the type system".

We are just in a special case where the "ahead" is already "here" because the type system is still behind the language. But even after it catches up, the situation will occur again. (Just as an example of evolution in action, as we start using tables in stringly-typed ways, that will be another place where we might need this.)

In short, this is not a phenomenon that ever finishes in a language where the dynamic semantics leads the static semantics.

Also, I don't think we're giving it any kind of complicated "semantics". It's just "error: feature not yet supported" in every case.