type-checker ignores top-level type annotations

[shriram]

The following program successfully typechecks:

double :: Number -> Number
fun double(s :: String): s + s end

Though I know the run-time Pyret ignores the first line, I think the type-checker should not.

[blerner]

All of Pyret ignores top-level annotations. We don't yet weave them in to the main program, because we haven't figured out the scoping/name resolution rules yet. They're just dropped on the floor.

[shriram]

I understand that. I'm asking @mkolosick to pick them up from the floor. In a typed language, it is not reasonable for this to be part of the syntax and yet not checked at all.

[blerner]

This does not sound like the right approach to me at all. The typed language shouldn't have to reconstruct these annotations (which, btw, it cannot do since they're no longer even part of the AST that it receives) and decipher which ones goes with which definition. The desugarer ought to do that, and weave the annotations in somehow, in a manner yet to be designed. Then you get dynamically checked annotations as well as static type checking. But the static system should not be responsible for doing this particular bit of work.

It's another whole design problem to figure out how to do name resolution here. There are at least a couple of problems: first, these annotations are forward-declarations, so there's no Name for them to resolve to yet. If you had

foo :: X -> Y
... lots of intervening code ...
fun foo(...): ... end
shadow foo = ...

it's not clear what the contract line should resolve to. Second, we need to decide what to do about examples like the one you gave, where the name is contracted and the definition is also annotated. It's a halting-problem task to decide if those annotations are equivalent, in general. Do we want to make your example be a well-formedness error (i.e. you may write either contract or annotations, but not both; this would be my preference), or do we want some brittle textual-equality check to see if the annotations "match" somehow, or something else?

I think there are other design issues involved, though I don't remember them all. This does not seem to be a high-priority problem right now, and requires a moderate amount of designing before it can even make progress.

[shriram]

Fine. In the interests of not turning this into an endless thread, how about we signal an error if someone uses this syntax?

[shriram]

Fine. In the interests of not turning this into an endless thread, how about we signal an error if someone uses this syntax? Or at least a warning saying that it isn't checked at all?

[blerner]

That's up to @schanzer. We enabled this syntax at his request, and he was fine with it being silent. (He was also fine with it being a comment, but preferred that it be syntax that we one day figure out how to enforce.)

[shriram]

I like being able to write it, and I'm sort of okay with it not being checked in the untyped language, because we don't check deep annotations either — the whole thing is sort of broken in a way that nobody seems to mind too much. But not checking in the typed language, were we do check all annotations, seems very, very wrong.

[schanzer]

If we need to back to comments to make the typed language consistent, that's fine by me. Would have been nice to have the option, but it's very low-priority on our end.

[blerner]

Making this work fully will also require adding new syntax for polymorphic annotations, since you can't write a polymorphic type just in an annotation at the moment (so you can't write the contract for map for instance). I don't much like adding warnings for features we do intend to support, but I also don't like the opportunity cost of yanking this syntax away right now... Joe, what's your take on this?

[blerner]

@shriram this seems to be handled now that contracts are woven into the program: the original program is illegal because you define the contract twice (once above, once inline with the definition), and if you make the definitions consistent, then you'll get a type error as desired if you call the function incorrectly. Confirm and close?

[shriram]

Almost. If I now swap the two lines:

fun double(s :: String): s + s end
double :: Number -> Number

I get an odd error that includes the phrase that the second line "does not match the name of any function definition", which is patently not clear. Fine if you'd rather close this issue and make a new one to address the wording of the error message on that one.

[blerner]

That's a by-design issue: when we talked about weaving annotations onto definitions, we all agreed that the annotations must precede the definitions. (It's technically infeasible to handle name resolution without imposing an ordering.) I really don't want to revisit and rehash that design choice here, since the weaving code is already a bit fiddly. I'm not convinced it's a major issue here since if you're following a DR scaffold, you'll write the annotations first anyway....

[shriram]

I think you're missing my point. My point is not "we should support annotations that come after the definition". It's that the current wording of the error message is bad because it says something that is patently untrue.

[blerner]

I understand that, but you're missing mine: I don't know how to detect that "patently untrue" situation, since name resolution doesn't help at all here.

[jpolitz]

The common cases that matter for this use the same name at the same block level, where we can check with un-resolved names. It should be only a little more sophisticated than ensure-unique-ids, which is already in well-formedness as a pretty simple check.

On Thu, Apr 12, 2018 at 5:14 PM, Ben Lerner notifications@github.com wrote:

I understand that, but you're missing mine: I don't know how to detect that "patently untrue" situation, since name resolution doesn't help at all here.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/brownplt/pyret-lang/issues/784#issuecomment-380982017, or mute the thread https://github.com/notifications/unsubscribe-auth/AAHUU1g-W5_JpBax0vmvEJCa1w0ZOHpaks5tn-3egaJpZM4JXfx5 .