From: LICS 2010
Date: March 21, 2010 2:36:57 PM CEST
To:
Subject: LICS 2010 notification
Dear author(s),
We regret to inform you that, due to an unsually strong competition this year,
your paper has not been accepted for presentation at LICS 2010.
Enclosed are the reviews. We hope that you will find them helpful.
---------------------------------------------
Paper: 55
Title: On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory
---------------------------- REVIEW 1 --------------------------
PAPER: 55
TITLE: On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory
This is an interesting paper on the timely topic of polymorphism in dependent type theory. As proof and programming systems for dependently typed languages are becoming more widely used, the importance of polymorphic notation is becoming more and more apparent. This paper provides an interesting proposal for a basic polymorphic predicative type theory with decidable type-checking. It may well have important practical consequences.
The paper builds on previous work by Miquel on the Implicit Calculus of Constructions (ICC) and a Church-style version ICC* by Barras and Bernardo. The point is that ICC* (without subtyping) in contrast to ICC has decidable type-checking. (The formulation on (p2,c1) could however be clearer.)
Abel introduces a predicative version (IITT) of ICC and builds a PER-model to prove consistency. Abel's model is simpler than Miquel's since he does not need to model impredicativity. Importantly, Abel also provides a type-checking algorithm which simultaneously removes implicit abstractions and applications. Decidability of type-checking is a key property of the most popular dependently typed languages, so is important to maintain. Unfortunately, Abel does not explain exactly what Barras and Bernardo proves and what the differences between ICC* and IITT are. One difference is that ICC* is based on untyped conversion whereas IITT has a typed equality judgement, but what else? The exact relationship between ICC, ICC* and IITT is crucial for the assessment of Abel's paper. For example, is the "suprising twist in the application rule" (p10,c1) an idea which is original to Abel. It should not be necessary to read the papers about ICC and ICC* in order to find the answers to such
questions.
Correctness of the type-checking algorithm is left to further work. This makes the paper a little preliminary. However, Abel has done much work on type-checking and normalization for dependent types, so will be in a good position to complete this work.
Generally, the paper is quite well-presented. Abel explains related work clearly, and goes on to present his type theory and its model in a standard way. A negative point for the presentation is that the paper does not quite make up its mind how to deal with variables and substitution. There are both de Bruijn indices and de Bruijn levels, and there are locally nameless variables. Then there is a substitution calculus. The reasons for this variety do not seem very strong and The ideas of the paper are not dependent of such low level issues and I suspect it would be clearer if the author tried to keep closer to standard lambda calculus notation.
The English is a little idiosynchratic in places. This applies both to word order ("to express in one language programs") and choice of words (to "devise" a language, to "honor" subsorting). Generally, the paper could do with a bit more proof reading "programs contain some to excessively much"), just to mention a few examples from the beginning of the paper. I also have my doubts about the chosen terminology. For example, is it not more common to talk about "dead" code than "static" code here?
Here are a few detailed comments.
p1,c1 -4. What is meant by "the universe-based approach"?
p2,c1, +12. There must be a typo, surely the target type of length should be Nat?
p3,c1, +10. What is the status of arities? Is succ standing alone a term or only succ t?
p3,c2, +20. To use the first argument C of natrec in index position is not official notation.
p3,c2,middle of page. What is a "resurrected" context?
p4, I would appreciate a clear account of the relationship between the typing rules here and of ICC.
p7,c1,+8. The key definition in the paper is the per associated with forall-types. The discussion could be expanded here. Is this definition the same as Miquel's?
---------------------------- REVIEW 2 --------------------------
PAPER: 55
TITLE: On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory
Working with dependent types often requires programs to be decorated
with terms (for proofs or for other kind of data), which do not
contribute towards the computation of the end result, but are used
solely for guiding the typechecker. These terms are called
"irrelevant", and one typically wants to remove them before the
execution.
Often times, however, it is not always clear which terms are
irrelevant and which are not. In the existing standard type theories,
such as Coq, one usually presupposes that every term of type P : Prop
is irrelevant, but this is often too conservative. For example, a
natural number used as a parameter to a dependent type (e.g., the
bound on the size of some list or array) is also irrelevant, but has a
non-propositional type.
Thus, it would be useful to have a mechanism in the language whereby
one can declare terms as irrelevant on a type-by-type bases, rather
than wholesale for a whole universe of propositions.
There have been a few works lately, mainly by Miquel and Barras and
Bernardo, which explore this topic from the perspective of
intersection types in the Calculus of Construction.
The current paper builds on that work, and irons a few kinks, but in
my opinion, the paper doesn't actually look quite finished yet, and
the main points are not very well-argued, or supported by theorems.
The author starts by observing that both the calculi of Miquel and
Barras and Bernardo have undecidable typechecking (the real problem)
and use an untyped conversion relation (a technicality, when compared
to the real problem). Then we are presented with a new calculus, which
has a typed conversion relation (or more precisely, a judgment for
comparing terms for equality) but where typechecking is still
undecidable, for reasons that are exactly the same as in the calculi
of Miquel and Barras and Bernardo.
However, as the author observes in the abstract, in the conclusions,
and throughout the paper, having typed conversion is better: it lets one
have eta laws for sigma, unit and empty types, and the presentation of
the models is simpler. Unfortunately, I'm not sure that this is a
reasonable comparison. Miquel's models support impredicativity, and
the current calculus is predicative. Moreover, the author does not
actually use eta-conversion (page 9, first paragraph states that we
only check programs in beta-normal form), and does not support sigma
types either.
From the presentational point of view, the main difference from the
mentioned calculi is a new typing annotation for irrelevant variables,
inspired by, but semantically different from the annotations used in
the type system for proof irrelevance by Pfenning.
For example, where Barras and Bernardo have a typing rule
G, x:A |- M : B
---------------------------------- x \notin FV(M*)
G |- \lam[x:A]. M : \forall x:A, B
the current paper has a rule which -- had the authors used variables,
instead of deBruijn indices -- would have looked like:
G, x%A |- M : B
----------------------------------
G |- \lam[x:A], M : \forall x:A, B
That is, the variable x itself is labeled as irrelevant, instead of
relying on a side-condition x \notin FV(M*).
This enables a few other changes, most notably, adding the inference
rule APP2
G |- t : \forall x:U. T G^\oplus |- u : U
--------------------------------------------
G |- t u' : T u
Here G^\oplus is the context obtained after removing the irrelevance
annotations. Notice that the conclusion uses the term u', not u. u'
can be arbitrary, possibly ill-typed expression.
The rule APP2 has somewhat of a special status in the calculus, but
the explanation of this status is a bit obscure, at least as far as I
could tell. The rule is essential, because without it, the theorems
don't work (e.g. Theorem 2, proposition 3). On the other hand, it
directly leads to undecidability, precisely because u' may be
ill-typed, just as similar problems lead to undecidability for Miquel
and Barras et al.
So what does this mean vis-a-vis the other existing calculi for
intersection type? Has this paper solved the problem with
undecidability? Or is its contribution only a minor reformulation of
the existing work?
Well, this is not quite clear to me, but I could make a guess.
If I understood correctly, the point is that the presented calculus is
really an internal calculus, and one would actually never typecheck
source programs in it. Rather, we will use a new system, which
combines typechecking with extraction, given in Section 5, where the
rule APP2 is not present.
This seems fine, but unfortunately, no theorems are presented to
confirm this intuition, nor are there any theorems which relate this
system from Section 5 to the one from Section 2, or to the evaluation semantics and
explicit substitution from Section 4 and 3, respectively. Without such results,
I'm afraid that the whole point of the paper is lost, and we are only really left with
a bunch of disjointed systems which are never put to use for a common purpose.
This is why I feel a bit unsure about recommending this paper for
acceptance. I think it has a potential and is showing a promising
direction, but it seems not quite finished and not particularly well
explained to me.
---------------------------- REVIEW 3 --------------------------
PAPER: 55
TITLE: On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory
This work aims to develop foundations for extraction of efficient programs from type theory.
The paper presents Implicit Intensional Type Theory, shows consistency by a partial
equivalence model, and presents a bidirectional type checking and extraction algorithms.
There is also some discussion of a notion of irrelevance. The presentation is not very clear
on why certain design choices are made.
---------------------------- REVIEW 4 --------------------------
PAPER: 55
TITLE: On Parametric Polymorphism and Irrelevance in Martin-Löf Type Theory
This paper introduces a predicative version IITT of Miquel's Implicit
Calculus ICC and studies its properties, including its partial
equivalence model. ICC is an impredicative system and IITT is
obtained from ICC by dropping its impredicative features. However,
because predicativity gives simplification, IITT has interesting
inference rules for irrelevance and a simpler model. It will give a
good framework for program extraction in predicative type systems.
Its main results are not so striking for a LICS paper, because the
main system is a fragment of a known system.
The paper is well written.
List of questions.
In the abstract, "a solid an practical" should be "a solid and practical."
In Section 1.2, I do not clearly see what is the goal of this paper.
If it is making the system ICC predicative and seeing what happens, it
would be better to mention it.
In Section 1.2, the definition of "implicit quantification" is
missing.
In typing rules in Page 3, uparrow is not defined.