Stefan pushed to branch report/tcvi at Stefan / Typer
Commits: 67371831 by Stefan Monnier at 2019-11-21T16:29:56Z Add a few FIXMEs while I have them in mind
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -426,6 +426,18 @@ Here we present the notion of erasability we use in the rest of the paper. \label{fig:epts} \end{figure}}
+\FIXME{ + Talk a bit more about the different kinds of erasability + %% - There's the one for Coq's Prop and sProp which is similar to "does + %% not affect the run-time". + %% - There's the one that says that dependencies can be erased in CC + %% (mentioned in Abel's thesis, probably means that you can erase + %% them and still get a well-typed term). + %% - There are more fine distinctions mention in the equality paper of Abel + %% where he distinguishes those where they can't be used in a dependent + %% way, and the one restricted to parametricity, etc... +} + The calculi we use in this paper are erasable pure type systems (EPTS) \cite{MishraLinger08}, which are pure type systems (PTS)~\cite{Barendregt91b} extended with a notion of erasability. We use @@ -1328,6 +1340,30 @@ not in general sufficient to tame the excesses of impredicativity.
\section{Universe polymorphism}
+\FIXME{ + Look at Nuyts's work on parametricity and impredicativity + %% There is appendix C in the extended version of our own paper: + %% https://people.cs.kuleuven.be/~andreas.nuyts/paper-reldtt.pdf + %% (Warning: the paper itself is extremely dense.) + %% However I was hesitant to pass this immediately as a reference because we + %% are by no means the inventors of this approach and maybe the appendix + %% doesn't emphasize that enough. + + %% Doing dependent elimination of Church encodings (ignoring predicativity + %% issues) WITHIN dependent type theory seems to be possible since the + %% work of Guilhem Moulin - see his PhD thesis: + %% https://www.chalmers.se/en/staff/Pages/guilhem-moulin.aspx + %% - though it seems he was so occupied by cracking the technical problem of + %% having internal parametricity operators that he didn't get around to + %% explaining how to use them. So in this sense I think we *may* be the + %% first ones to spell out how to do this within DTT. + + %% However, similar ideas can be found in earlier work using predicate logic + %% over simple type systems. For example Wadler has some stuff to say about + %% induction on the natural numbers: + %% https://doi.org/10.1016/j.tcs.2006.12.042 +} + While paradoxes like Hurkens's suggest that it is impossible to have impredicative definitions in more than one universe without losing consistency, inductive definitions suggest otherwise. @@ -1366,8 +1402,10 @@ type system could be described as the following EPTS: k \in {\kw{n},\kw{e}}, \ell \in\mathbb{N}, \ell_2\in\mathbb{N}\cup{\omega} ~} \end{array} \end{displaymath} -So it would place our universe-polymorphic definition of \id{NatL} above -squarely in the far away $\Type{\omega}$ universe. Yet everything that can be +So it would place the above universe-polymorphic definition of \id{NatL} +squarely in the far away $\Type{\omega}$ universe. +%% FIXME: Can we make this "everything" argument more formal? +Yet everything that can be done with it can also be done with the real \id{Nat} inductive type, which lives in the much more palatable $\Type{0}$ universe, so it would arguably be safe to let \id{NatL} live in $\Type{0}$ (and thus make this definition @@ -1386,6 +1424,8 @@ not inherently incompatible with consistency. Of course, this begs the question: what is it that makes it safe to let those definitions be treated as impredicative? What is special about them?
+ + %% \section{Related work}
%% \nocite{Gimenez94}
View it on GitLab: https://gitlab.com/monnier/typer/commit/67371831c77e631c217f3847ba774e090322...
Afficher les réponses par date