I didn’t get a chance to put together a post on Friday, but I made some decent progress. Here’s a short recording of an editing session:
A few notes about what’s happening here:
□ : Numberindicates that the current location has the type
Conceptually, the explorer is just providing a very structured way of selecting a replacement value for the current edit location. But it is restricted to choosing values which ensure the resulting expression is still well-typed. This is where the admissible type comes into play. The admissible type must be the subtype of any chosen replacement, so for instance
forall a . a -> a is a subtype of
Int -> Int (any function expecting an
Int -> Int may safely be given a
forall a . a -> a). This is not ‘subtyping’ in the OO sense, it’s the subtyping relationship induced by use of quantifiers.
The current type and the admissible type can coincide, though it will always be the case that the admissible type is a subtype of the current type. But, for instance, when replacing the body of the lambda
x -> 42, since nothing else constrains what the lambda must return, the admissible type is
forall a . a (or unconstrained). If we had a type annotation that was being pushed down into our expression, or if our lambda were named and used elsewhere in a way that constrained its output type, that information would be reflected in the admissible type.
Last week I gave a proposed interaction for how to search for terms at more global scope. I suggested that if the explorer is open, adding a
? to the front the the search string will increase the search to include global scope. And we could imagine having some other syntax to control the scope of search, to, say, only terms defined in the current panel, or constrained to some package, where a package is just some metadata which points to a bag of terms.
While it might be nice to have the ability to define the scope more precisely, I actually think it’s a better user experience to just make the default scope include everything, and simply display any relevant metadata the user might need to make their selection (or further refine the search). The reason I prefer this is that it’s less work for the user in the cases where the context is sufficiently discriminatory, which is often the case in typeful programming. That is, if the context is sufficiently type-constrained, we can just give the user all results, from all scopes, and free the user from having to decide what rather arbitrary ‘bin’ to start their search in. And if there are too many results, we can order the results intelligently, indicate there are more results to be had, and put the user in charge of refining their search now that it has proven necessary. Of course, the user can still narrow their search to whatever scope up front, it’s just this isn’t the default.
That’s all for now, more updates later this week.comments powered by Disqus