9
$\begingroup$

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ is. It seems to be identical to $CC$ except there is a distinction between implicit and explicit arguments for functions. In particular, I don't see how it allows you to write $(id\; 0)$ instead of $(id\; \mathbb{N}\; 0)$. If we assume a system for global definitions, then,

$id : (\Pi A\; |\; \mathsf{Type}\; . (\Pi x : A\; . A))$

and

$id = (\lambda A\; |\; \mathsf{Type}\; . (\lambda x : A . x))$.

Do the rules really allow for $(id\; 0)$? Of course the syntax does, but I don't see it in the typing relation. Am I missing something? Am I understanding the role of $CC^{bi}$ incorrectly?

Also, isn't the property of confluence lost? I guess my problem is that I'm reading about elaboration without having read much about $CC^{bi}$ before this. What's a good paper that introduces it and it alone?

Edit: To be more specific, I am asking how $(id\; 0)$ is accepted in place of $(id\; \mathbb{N}\; 0)$ when the rules for both explicit and implicit $\Pi$ application are identical modulo sytnax. I see no difference between $:$ and $|$ the rules for both seem the same.

Edit: I am not talking about the Implicit Calculus of Constructions, which is a different theory and has different rules for explicit $\Pi$'s (application vs. generation.)

Edit: Okay, I think I'm starting to understand this but I won't answer this question until I'm sure. Basically $(id\; 0)$ does not type check and in fact it is just elaborated to $(id\; \mathbb{N}\; 0)$ right before type checking or done as a secondary responsbility of the type checking algorithm. Essentially these implicit calculi are intended to be interface (user-end) languages which are elaborated into the usual (explicit) calculi or at least the explicit fragment of the implicit calculi before the terms are type checked. If that is the case, then I think I see the big picture. Can someone please confirm this?

$\endgroup$
  • 2
    $\begingroup$ As i said below, your intuition is correct: the bi-colored calculus of constructions is an explicit calculus, in which the arguments omitted by the user but elaborated by the "front end" are explicitly marked. Also, confluence is lost for beta+eta reductions, but true if restricted to only beta. $\endgroup$ – cody Jul 29 '11 at 9:01
9
$\begingroup$

In The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping, Alexandre Miquel introduces the basic concepts for the Implicit Calculus of Constructions, which I believe is synonymous with the Bicolored Calculus of Constructions.

The point is (among other things) to have a calculus without the clutter of explicit type annotations everywhere. Type inference is (very likely to be) undecidable though.

In this calculus, if we take $id=\lambda x. x$, then you can derive $$ \vdash id\colon \forall X\colon Type. X\rightarrow X$$ by simply using the explicit product and the implicit product rules in succession. Then the instantiation rule for the implicit product allows $$ \vdash id\colon Nat\rightarrow Nat $$ and so $$ \vdash id\ 0 \colon Nat$$ The system admits subject reduction and confluence, even on untyped terms (which in fact fails for calculi with abstraction annotations). All this can be found in Alexandre's thesis, which is sadly in French. Not sure I have a better reference for these results though I'm afraid.

$\endgroup$
  • $\begingroup$ The first part of your answer I did know but I think I should have been more specific in my original question. That is, how exactly is (id 0) allowed if id has the type (\Pi X | Type . X -> X) because it seems like APP rule is identical for both the implicit and explicit \Pi. In the implicit calculus of constructions, which is in fact a different theory, this is not the case because it's seperated into APP and GEN. For verification that it is different, check the heading "A Calculus with ‘really implicit’ arguments" in the paper that you referenced. $\endgroup$ – Anthony Jul 29 '11 at 2:57
  • 1
    $\begingroup$ Regarding decidability. The paper that you reference conjectures that it's theory is undecidable. The paper that it references (I guess the "original" bicolored calculus of constructions paper) claims to be decidable but does not explicitely prove it. I read it after I posted this question and it seems that it definitely should be decidable and depending on the syntactic restrictions retain confluence. On the other hand, I am still stuck with my original confusion :\ $\endgroup$ – Anthony Jul 29 '11 at 2:59
  • $\begingroup$ Maybe you should tell us which paper you are looking at. $\endgroup$ – cody Jul 29 '11 at 8:11
  • 2
    $\begingroup$ Ok, I had a look at Elaboration and Erasure in Type Theory by Marko Luther, which I am guessing is your reference. In that case, there is no semantic difference between the explicit and implicit products, and indeed the bi-colored system is a conservative extension of the calculus of constructions. What happens is that you use elaboration to take a term without the explicit argument to turn it into a fully annotated term: id !1 0 elaborates to id Nat 0. In this text, elaboration is covered in section 4. $\endgroup$ – cody Jul 29 '11 at 8:58
  • $\begingroup$ Yeah that is the paper I started on, I just hadn't passed the part on the usage of $CC^{bi}$ nor did I realise how he was developing one theory on top of the other sequentially and that the earlier developments are only use as pedagogy. Forgive me for not mentioning it earlier, I thought the calculus was well known by its name outside of paper I was reading. $\endgroup$ – Anthony Jul 29 '11 at 10:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.