type-checker ignores refinements

[shriram]

A student expected the following to type-check:

fun f<A>(lst :: List<A>%(is-link)) -> List<A>:
  lst.rest
end

[Credit for request: Louis Kilfoyle.]

[mkolosick]

Do we want to allow students to write this? My main issue with the feature is that I don't have a good way to handle its interaction with imports. If a user imports a different function as is-link I don't currently have a way to tell that this function is actually the predicate.

[blerner]

It's much slipperier that that. The identifier in refinement position could be any function. The next step up from this "not empty list" is a "not empty tree", and we don't have any built-in way to write that as a refinement when there are more than 2 constructors for the data type. Supporting that would basically imply that we solve dependent types for Pyret, and I don't think we want to go there. The alternative is to say "we can type check refinements when the refinement is a single constructor predicate, but nothing else, sorry." And I think that's a recipe for frustration.

[shriram]

I'm not sure I agree w/ Ben's "recipe for frustration". I feel the pattern this student has written occurs somewhat often (I've seen it when writing interpreters, certainly).

I'm not sure what is gained by writing the same one-liner as a four-liner with a cases and forced error, etc. — especially if I have some other invariant that says we won't hit that situation.

[blerner]

But what's the pedagogy that lets you say "You're allowed to typecheck List%(is-link) but not Tree%(is-balanced)"? Why can't I write that and use that invariant? Sure looks syntactically the same! Ok, maybe that's too complicated. But if I have a 2-3-tree, why can't I write TwoThreeTree%(is-not-leaf) and typecheck using that?

[jpolitz]

I would be happy saying:

“Great question! You can type-check variants in refinements but not arbitrary predicates, because the type-checker would need to run your code to do that. (Side note: You actually can do some of this in a type checker, come to office hours and we'll chat).”

It seems like a scope/environment bug that the URI of the identifier isn't available when setting up the type environment. That's something to improve for non-global information that's coming in (all imported identifiers should know their defining module).

[shriram]

I just got another question from a student about this. [Credit: Zachary Espiritu.] We published an assignment spec that listed a %(a-cases-predicate) in some signatures. The student wanted to know what to do with the other cases because the type-checker wasn't letting him run his code. He pointed out that of course his code worked just fine without the type checker — i.e., he could just switch away from it and be happy. Since there are several functions with the refinement, it adds up to write all those extra cases.

And just to reiterate, I think Joe's response is great. I mean, there are all sorts of other places where we work around the Halting Problem — heck, the type-checker itself. That doesn't keep us from using a partial solution.