CTT Example

[jonsterling]

This is the beginning of a PRL for a variant of CTT.

I really want to get #11 done, since I have this really cool idea for a way to formulate a PRL for CTT using it that has about half the rules (basically, all structural equality rules become derivable, and I have in mind a handy tactic for deriving them, which we could define).

[david-christiansen]

This is starting to look nice :)

It does look like the elaborating type checker for LF terms should be a fairly high priority, though.

[jonsterling]

It does look like the elaborating type checker for LF terms should be a fairly high priority, though.

I think I agree... Are you referring to addressing the bureaucratic aspects of forming variable applications in context (e.g. ($* X Γ))? or to something else?

[david-christiansen]

That and the typos that you fixed in d838601 :)

[jonsterling]

oh, lol :) Yeah. Somehow I think we can prevent that using contracts and maybe even the current typechecker... not sure though.

Am 13.06.2017 um 22:49 schrieb David Christiansen notifications@github.com:

That and the typos that you fixed in d838601 :)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[david-christiansen]

Mostly. The difficulty is that the type checking has to happen relative to an ambient signature, and we don't want to have to write the names of signatures all over the place.

What might work, though, is for each signature to give rise to an explicit quotation form that type checks at macro expansion time. This would also require a way of extending signatures to be practical, I think.

Something like:

(define-signature ctt
  ...)

(define-signature ctt/nats #:extend ctt
  ...)

(define test1 (ctt (lambda (x) x)))
(define test2 (ctt/nats (lambda (x) (succ x))))

So rather than defining macros directly for LF terms, we would have a meta-macro for each signature that type checks and elaborates the syntax in the signature. What do you think?

[david-christiansen]

The elaborating bit is also orthogonal - the current type checker could be used to make an explicit version of this approach.

[jonsterling]

@david-christiansen I am a bit worried that it doesn't suffice to just remember what signature we were in—in general, we may be working with open terms, so we would need to know further context, right? Or maybe this is not the case...

[jonsterling]

Knowing only the signature may actually suffice, since in all the cases that I can think of, we should know enough to supply the extra context...

One wrinkle is that the intermediate states of the proof refinement engine are not necessarily well-typed. The reason for this is that we are using the LF's (TYPE) to classify "refinements" / judgments, whose relation to their extracts is not really reified in the system. For instance, we treat x:is-inh(A) as if it were x:tm; if we could "erase" all these refinements, then the terms would be well-typed.

[david-christiansen]

You're right, context would be necessary. I wonder if that can be solved by annotating free variable objects from the locally-nameless code with signature/type pairs. That'd potentially allow Racket binding to propagate enough of the context.

[jonsterling]

The issue with these "refinements" is what I alluded to on the phone when we spoke—I don't yet know how to understand these constructions INSIDE of LF, so I have had to be content to work with this extrinsic erasure invariant (which is not totally satisfactory to me).

[david-christiansen]

Ah, OK. Perhaps the extrinsic bit can at least be systematized with a bit of macrology.

[jonsterling]

Ah, OK. Perhaps the extrinsic bit can at least be systematized with a bit of macrology.

Yeah.

[In what follows, I am overloading the word "refinement" in a very bad way, so be cautious.]

Also, I think that I might be thinking about these refinements from possibly the wrong perspective. I think maybe the right way to look at it is to follow Zeilberger & Melliès and think of these judgments as forming a category fibered over the classifying category of the main LF signature.

One way to capture this is to define a second LF signature for the refinement layer, but without any term operators. Then, the morphisms for the refinement layer are defined by the LCF-style rules that are given. Here's what I had in mind:

(define-signature CTT
 (tm (TYPE))
 ....)

(define-refinements CTT-refinements CTT
 (<: is-inh ([A (tm)]) (tm))
 ....)

This generates an extension to the CTT signature with new types (is-inh A),... and presumably a function |-| to project away is-inh A to tm, etc. Then, a refinement rule can be read in the following way. A rule like

(define-rule rule-name (>> Γ J)
 ([x (>> Γx Jx)] ...)
 e)

shall presuppose (using contracts) that CTT, x : Π |Γx| |Jx| ... !- e <= Π |Γ| |J|; and this rule shall be regarded as a morphism Π Γx Jx ... ==> Π Γ J in CTT-refinements, which lies over CTT.

[david-christiansen]

I think I'll need to back-and-forth with you to understand this one. Let's talk further at OPLSS.