Kenji Maillard (Aug 27 2020 at 08:37): Kenji Maillard (Aug 27 2020 at 08:37):Looking naively at the typing derivations for PCUIC (found there), I was wondering whether the derivations are a property of the triple 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.
Gaëtan Gilbert (Aug 27 2020 at 09:06):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
Paolo Giarrusso (Aug 27 2020 at 10:45):Could you formulate an algorithmic version of pcuic, and relate it to the declarative version in the usual way?
Paolo Giarrusso (Aug 27 2020 at 10:45):That would turn the decider into a syntax-directed type system
Kenji Maillard (Aug 27 2020 at 11:17):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) ?
Kenji Maillard (Aug 27 2020 at 11:19):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.
Gaëtan Gilbert (Aug 27 2020 at 11:37):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
Paolo Giarrusso (Aug 27 2020 at 20:09):hmm, how would you write the other typing rules? would you use |- or |-0 ?
Paolo Giarrusso (Aug 27 2020 at 20:11):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.
Paolo Giarrusso (Aug 27 2020 at 20:13):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 (?)
Gaëtan Gilbert (Aug 27 2020 at 20:24):it's possible i got it wrong
Paolo Giarrusso (Aug 28 2020 at 06:20):Mine is more a question than a statement :-)
Meven Lennon-Bertrand (Aug 28 2020 at 09:15):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: May 31 2023 at 09:01 UTC