# What is the role of the Bicolored Calculus of Constructions?

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?

• 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. – cody Jul 29 '11 at 9:01

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.
• 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. – cody Jul 29 '11 at 8:58
• 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. – Anthony Jul 29 '11 at 10:36