peterlefanulumsdaine / general-type-theories Goto Github PK

Ideal end goal: a reflection-style notation, with something like a function var_of_nat (i:nat) (p : le_dec i n = true) -> (fin_context n), and then a notation "$ i" := (var_of_nat i refl).

i.e. complete notation [S/ A ; e1 , … , en /] as sketched in files, along the lines of [M/ A ; e1 , … , en /]

Complete them, as itemised as TODO’s

Probably needed in order to define morphisms/extensions of signatures.

Will require replacing the straightforward family sum in Metavariable_Extension with a roll-our-own inductive family.

Currently, a judgement form instance is a function forall i : Slots jf, Raw_Syntax Σ (val i) γ.

This means that they don’t have a very well-behaved judgemental equality, which will be a pain in the arse when we are trying to give actual derivations. If they can be inductive/record types, life will be much easier. However, as we saw originally, giving them by hand as products/sigmas made acting uniformly on them very clunky.

Proposal: perhaps we can get the best of both worlds by defining slots jf as a list of syntactic classes, and then using a forall_list construct which computes down to an iterated product. I.e. a judgement form instance is forall_list (slots jf) (fun cl => Raw_Syntax Σ cl γ).

I would like to rename several concepts, but I think we should discuss them before I do it. It is very important that we name things so that people can understand what is going on. If we end up having "proto contexts", "raw contexts", and "well-done contexts" that will be a bit cumbersome.

Cxt

Let's start with one that is irrelevant but annoys the hell out of me. Contexts should be abbreviated as ctx instead of cxt. I repeatedly mistype this because in other pieces of software (Andromeda, for instance) it is ctx.

Shape system

Next, I think Proto_Cxt is a misnomer, and so is Shape_System. As far as I can tell a shape system is a structure which describes possible binding contexts, such as the ∏x:_, _(x) and x:_, y: _(x) ⊢ _. This is about bound variables. In a sense, we never have any free variables, since they are "bound" by the typing context. It is wrong to call an element of Shape_System a Proto_Cxt because it might be used to describe something related to ∏, which has nothing to do with contexts. So, mu suggesting is:

• Shape_System should be called Binding_structure
• An element of Binding_structure should be called simply binding. We use it a lot, so a good single letter for it would then be B.

Raw

A bunch of things are called "raw". There is "raw syntax" and "raw rules". As we know, the phrase "raw" is used for "raw syntax" in type theory. I do not actually think that there is anything "raw" or "pre" about it. It's just syntax, but not all of it is well-typed.

For instance, in programming languages we speak about the syntax of expressions, and some expressions are well-typed, but there are also syntactically correct ill-typed expressions. The syntax is what the parser handles.

My suggestion would then be that "raw syntax" is just "expression", as far as I can tell, since it is either a variable or a term former applied to stuff.

It is a bit harder to put "raw rules" and "rules" in order. We have three entities, it seems:

• the syntactic form which describes a rule
• the corresponding closure condition
• the syntactic form describing a rule together with evidence that it is well-formed

The closure condition is named correctly already. We need to distinguish between the syntactic rule, and the rule which is well-formed or valid. Can we find two different words for these? For instance "rule schema" and "rule"? A "rule schema" is the syntactic form which displays a rule, but it is not a rule unless we verify that it is well formed?

As documented in the file, for general shape-systems, not every context is an iterated extend_shape, so it’s not enough to formulate the context-extension rule just using extend_shape. Possibilities:

1. restrict (somewhere down the line) to a shape system like de Bruijn where every context is literally an extension; then the basic rule is indeed enough.

2. formulate the “context extension” rule such that it applies not literally just [extend_shape], but to any “one-element extension”. (Then give the basic cxt-extension rules as derived.) (Issue: doesn’t respect extra structure a shape system may carry, e.g. ordering of variables, which everything else does currently respect.)

3. besides the basic rule, give a “renaming of variables up to isomorphism” rule. (Issue: inconvenient to use in derivations. Also, again doesn’t respect extra structure.)

4. (more radical) just ask a context to show that all its types are types over it; to make this possible, allow substitution into arbitrary raw contexts. (Other rules will still only work over actual contexts.) (Issue… just WTF. Not at all clear to me (PLL) how one would give interpretation for this approach, even over a specific simple shape system.)

1 seems fine for the de Bruijn shape system. 2 and 3 seem rather ad hoc. Can we find a more elegant solution??

i.e. over concrete shape systems, substitution should compute well. Give some examples to check that it does!

as a first example of a logical raw rule (i.e. not just structural)

I.e. check that boundaries of all judgements involved are derivable