search

jonsterling / racket-grit

Grit: the kernel around which a PRL forms
Other
3 stars 0 forks source link

Wellformedness coercions #13

Closed jonsterling closed 7 years ago

jonsterling commented 7 years ago

I had a thought...

By imposing some kind of abstraction, we can ensure that it is not possible to construct a raw term in which the non-wellformed part is anywhere other than the outer layer of syntax. For example, we can write a "term" x which needs to be converted to (Λ () ($ x)), but there's we can ensure that the user could never write something like (Λ () x). This means that we can design the coercions to only work with a single layer, and do no recursion; as a result, we can call these freely everywhere, which resolves a lot of the problems...

The place where this abstraction is currently broken is that the user could call the generic instantiate from the locally nameless library, and put some garbage in there. I think that this is another sign that we should somehow simplify how that works, and make it so that the user cannot use that low-level machinery manually—it should only be possible to use whatever substitution mechanism we export from the logical framework library.

This PR implements the idea about one-layer coercions, but does not yet address the abstraction breakage issue.

jonsterling commented 7 years ago

@david-christiansen I started trying to hook up scope to have this predicate attached to it which we described, but I got stuck... I can't remember exactly where I got stuck, but I ended up thinking that the design doesn't quite work smoothly. I can try it again and see if I can remember what went wrong.

jonsterling commented 7 years ago

Maybe a lighter-weight alternative would be to inline the locally-nameless module inside of the logical-framework package, and then NEVER provide/export the abstract and instantiate operations. We could provide instead things that did the appropriate checking or were protected by appropriate contracts.

david-christiansen commented 7 years ago

I really think we should abandon the generic approach to locally-nameless and just have abstraction and instantiation match directly on the LF syntax. This is far simpler, because it only supports extension through the signature, which is what we want. Right?

jonsterling commented 7 years ago

@david-christiansen That may be a reasonable idea, I'm open to it. The one issue is that it is nice to be able to re-use some of these structures, like telescopes, for different stuff; but we can no doubt accomplish that otherwise.

With that said, I was just playing around a little bit, and I think that my idea for a way to introduce malformed terms was faulty—that is, I don't think that I can use abstract and instantiate to embed a malformed term into the middle of a wellformed term. (This is essentially because the base-case for substitution, which is application, only allows substitution by a variable, which is renaming, or substitution by a lambda of appropriate valence, which is hereditary substitution.) So, if you try to do something bad, like substitute an application for a variable, you get an error. So, I think the wellformedness abstraction is not broken.

david-christiansen commented 7 years ago

OK, then let's leave it as-is for now. The Typed Racket angle is not relevant anyway due to lack of custom equal?.

jonsterling commented 7 years ago

@david-christiansen OK, that sounds reasonable.