Looking naively at the typing derivations for PCUIC (found there), I was wondering whether the derivations are a property of the triple $(\Gamma, t, A)$ or a structure over such a triple ?

For instance, are there lemmas showing that there is at most one typing derivation ? (likely not the case because conversion could apply anywhere)

Or if they are multiple typing derivations, whether a canonical one can be singled out ? (More likely if there are inversion lemmas) And if so, how it relates to the other derivations ?

Another related question is how reduction acts on such typing derivation. The proof of subject reduction shows that reduction can be lifted from terms to typing derivations but looking at the proof script it's hardly clear to me what's happening in the proof.

You can get a canonical one by running the decider

it will do something like interleaving structural and conversion steps, so there's never 2 conversions in a row

Could you formulate an algorithmic version of pcuic, and relate it to the declarative version in the usual way?

That would turn the decider into a syntax-directed type system

Gaëtan Gilbert said:

You can get a canonical one by running the decider

it will do something like interleaving structural and conversion steps, so there's never 2 conversions in a row

That's indeed a first step towards an answer to my question, but how "canonical" is the resulting derivation ? For instance, is it (proven to be) idempotent ? Can we give a high level spec of the shape of the generated typing derivations (beside the alternation between structural and conversion rules, which is already a good starting point) ?

Paolo Giarrusso said:

Could you formulate an algorithmic version of pcuic, and relate it to the declarative version in the usual way?

@Meven Bertrand was working on a bidirectional presentation of the typing, so he might be able able to answer our questions on that.

But even a syntax-directed system does not necessarily explain immediately how it relate to the non-syntax directed one.

Producing a derivation by the decider doesn't use the input derivation except in the aburd case where the decider says "no", so it must be idempotent

If you present your rules with conversion integrated, such that instead of

```
|- f : A -> B
|- x : A
========
|- f x : B
|- e : A
A <= B
=======
|- e : B
```

you have

```
|- f : A -> B
|- x : A
=========
|-0 f x : B
no constructor of |-0 for conversion
```

and `|- e : T`

defined as `exists T0, |-0 e : T0 /\ T0 <= T`

then you have no choice about where to use conversion so it's propositional (assuming the conversion judgment is propositional)

and there is a canonical translation from the second presentation to the first which I think produces what the decider would

hmm, how would you write the other typing rules? would you use |- or |-0 ?

That example looks weird — looking at subtyping, I’d usually expect `f : A1 -> B, x : A2, A1 == A2`

. Here -> might be hidden, but I’d still expect `|- f : T1, T1 ==HNF=> A1 -> B, x : A2, A1 == A2`

.

But even a syntax-directed system does not necessarily explain immediately how it relate to the non-syntax directed one.

By “relate it in the usual way” I imply also proving equivalence — TaPL shows how to do it for STLC+subtyping, I’m not sure I’ve seen anything fancier — at most they do F-Omega (?)

it's possible i got it wrong

Mine is more a question than a statement :-)

Kenji Maillard said:

Meven Bertrand was working on a bidirectional presentation of the typing, so he might be able able to answer our questions on that.

My feeling right now is that there is a gap in the formalization, namely a declarative, but bidirectional variant of typing, to mediate between the decider and the undirected declarative typing. This one I would hope to have some kind of uniqueness of derivation, corresponding to the derivation given by the decider when it succeeds, and giving a canonical undirected variant.

This canonical variant would correspond to what @Gaëtan Gilbert hints at, namely the one that concentrates conversion steps to the typing rules for eliminators (this is the only place where they are really needed).

A tentative description of such a bidirectional system is done in section 4 there https://hal.archives-ouvertes.fr/hal-02896776/document if you want to look at it, but I hope to investigate it for itself soon.

Last updated: Feb 22 2024 at 03:02 UTC