Support postulates.

[Toxaris]

Postulates would be convenient for rapid prototyping.

[Toxaris]

@Blaisorblade's idea in #98 motivates the following:

Proposal 1: Add a new kind of statement

postulate name : term;

that is processed as follows:

1. term' <- typecheckPull env term.
2. check that typeOf term' is a constant c.
3. check that c is a sort.
4. name' <- fresh name
5. extend the environment by (name, term', ResidualVar name')

The processing is motivated by thinking of postulate name : term; rest as Pi name : term . rest.

[Toxaris]

Proposal 2. Also parse postulate n1 n2 n3 : term; and postulate (n1 n2 : term1) (n3 : term2) etc. like for BindStmt, Lambda and Pi. Desugar to a sequence of postulate statements in the parser.

Discussion: One drawback of this is that it will be hard to teach to the .ctags.

[Blaisorblade]

I'm implementing (the semantics of) Proposal 1.

Following the example of #98, I'm not generating a fresh variable. Rather, I'm simply letting name evaluate to ResidualVar name. This clearly matches what big-step evaluation would do on a variable (which is more obvious than the correct behavior for a denotational semantic into a domain that contains syntax).

[Blaisorblade]

From looking at the parser, it seems we might want postulates with an argument telescope. OTOH, this is just sugar for the corresponding Pi-type:

postulate n1 (arg1 : t1) : t2; --equivalent to:
postulate n1: Pi (arg1 : t1). t2;

So for now I'm not supporting those telescopes for postulates. I'm also leaving out Proposal 2 for now (because of the drawback, and because I'm less sure of how to do the desugaring — it would need a bit of restructuring I guess, so that stmt could return multiple statements.

[Toxaris]

I agree that my proposal 2 is stupid.

I also agree that postulate n1 (arg1 : t1) : t2 should be allowed and should desugar to postulate n1: Pi (arg1 : t1). t2. The benefit of this seemingly boring desugaring is that one can move from:

postulate lemma (...) : ...;

To:

lemma (...) : ... = ...;

without changing too much code.

(So we could also support postulates without the postulate keyword, just by leaving out the = ... part).

[Toxaris]

Following the example of #98, I'm not generating a fresh variable.

Why? I clearly motivated the need to generate a fresh variable by comparison to Pi. And indeed, I just tested your implementation of postulates (as of 68e8a04) and found a problem with shadowing:

language stlc;

postulate foo : Int;
bar = foo;
postulate foo : Int;

assert foo = bar;

This should fail, but it succeeds.

Big-step operational semantics might avoid this problem by not reducing under binders. But the point of postulates is to reduce the rest of the file "under" the postulated binder.

[Blaisorblade]

In short: you made me realize I don't fully understand the underlying theory of bindings we use.

The processing is motivated by thinking of postulate name : term; rest as Pi name : term . rest.

I'd usually expect a lambda there, not a Pi. But the main point is still the same.

Why? I clearly motivated the need to generate a fresh variable by comparison to Pi.

Ah, I see. Thanks for the catch. (As we know from reading mathematics, "clearly" is a relative concept, but let's not discuss that).

I guess I didn't understand safebind yet and then I'm not sure why we don't need fresh bindings for #98.

But now I get it: safebind idea can be summarized as: if needed (because we're shadowing an existing binding), then generate a fresh variable. I think that (as long as we don't rewrite the typechecker in CPS) we might need a less-CPS-y version of safebind that we can reuse.

I guess this might be relevant also to #98: bindings that shadow each other and are both erroneous become equal in my current implementation.

Big-step operational semantics might avoid this problem by not reducing under binders.

Well, I suspect "produce closures when evaluating binding forms" is also relevant — would that not allow full normalization? Do we produce closures somehow (other than in the function values, using meta-level closures)? It seems we have a partially named, partially HOAS representation, and it confuses me. We understand postulates as lambdas, but then we throw away the lambdas.

More generally, is there a standard description for the freshening you do in safebind, or is it smart but ad-hoc (whatever "ad-hoc" actually means)? I mean, I can see why it makes sense in this example. And maybe I can make up a partial description: just apply bindings that shadow each other to different free variables, and you get the result PTS produces.

But the point of postulates is to reduce the rest of the file "under" the postulated binder.

And we do need to reduce under binders — in the PTS checking paper they use different reductions, including one that seemed weak-head reduction, but that's not what they usually use.

[Toxaris]

Yes, #98 also needs freshening.

Big-step operational semantics might avoid this problem by not reducing under binders.

Well, I suspect "produce closures when evaluating binding forms" is also relevant

We also produce (metacircular indeed) closures when evaluating binding forms, but then we open these closures with a fresh variable name in PTS.Dynamics.Evaluation.reify and PTS.Dynamics.Evaluation.equiv. Our treatment of postulates has to inline the calls to fresh in Evaluation.hs, kind of.

It seems we have a partially named, partially HOAS representation, and it confuses me.

We don't use HOAS.

We use meta-level functions in values and names in terms. HOAS would mean to use meta-level functions in terms, which we don't.

[Blaisorblade]

We also produce closures when evaluating binding forms, but then we open these closures with a fresh variable name in PTS.Dynamics.Evaluation.reify and PTS.Dynamics.Evaluation.equiv.

Good. What about the optimization in safebind (not freshening if not shadowing)? I still guess it's correct, but how do we make sure of that?

[Toxaris]

I think the paragraph starting with "At this point" on page 64 of http://www2.tcs.ifi.lmu.de/~abel/habil.pdf is relevant to this question. It contains a reference to http://edoc.ub.uni-muenchen.de/9761/1/BarralPhd.pdf which might or might not explain what we're doing. There's also a reference to http://www2.tcs.ifi.lmu.de/~abel/lmcs10.pdf which maybe describes what we should be doing.