<p>In <a href="https://www.fing.edu.uy/~amiquel/publis/tlca01.pdf" rel="nofollow noreferrer"><em>The Implicit Calculus of Constructions
Extending Pure Type Systems with
an Intersection Type Binder and Subtyping</em></a>, Alexandre Miquel introduces the basic concepts for the Implicit Calculus of Constructions, which I believe is synonymous with the Bicolored Calculus of Constructions.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2011-07-29T02:57:17.480Z
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.
Anthony
CC BY-SA 3.0
2011-07-29T02:59:18.260Z
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 :\
Anthony
CC BY-SA 3.0
2011-07-29T08:11:05.610Z
Maybe you should tell us which paper you are looking at.
cody
CC BY-SA 3.0
2011-07-29T08:58:47.720Z
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
CC BY-SA 3.0
2011-07-29T10:36:21.463Z
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
CC BY-SA 3.0
2017-08-10T22:36:13.997Z
Why not just annotate the CC with holes and use unification algorithms to complete it (e.g., as part of your code editor)? I mean, why make a different language, in what situation it could be useful for?
MaiaVictor
CC BY-SA 3.0
2017-11-16T02:19:51.523Z
The link is dead
Christopher King
CC BY-SA 3.0
2017-11-16T17:07:17.267Z
@PyRulez fixed the link (and added the title of the paper, to help with future breakage).
cody
CC BY-SA 3.0
2011-07-28T21:57:52.530Z
2017-11-16T17:06:35.797Z
2017-11-16T17:06:35.797Z
cody
<p>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,</p>

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

<p>and</p>

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

<p>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?</p>

<p>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?</p>

<p><strong>Edit:</strong> 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.</p>

<p><strong>Edit:</strong> 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.) </p>

<p><strong>Edit:</strong> 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?</p>

CC BY-SA 3.0
2011-07-29T09:01:27.780Z
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
<type-theory><lambda-calculus><type-inference><dependent-type>
What is the role of the Bicolored Calculus of Constructions?
Anthony
# What is the role of the Bicolored Calculus of Constructions?

(Asked by: username_0 on 2011-07-28)

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?

**Tags:** type-theory, lambda-calculus, type-inference, dependent-type
> **Comments:**
> **username_1**: 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.  

---

## 1 answers

### Answer by username_1 on 2011-07-28. Score: 9 | Accepted answer

In [*The Implicit Calculus of Constructions
Extending Pure Type Systems with
an Intersection Type Binder and Subtyping*](https://www.fing.edu.uy/~amiquel/publis/tlca01.pdf), 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.

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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 :\  
> **username_1**: Maybe you should tell us which paper you are looking at.  
> **username_1**: 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.  
> **username_0**: 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.  
> **username_2**: Why not just annotate the CC with holes and use unification algorithms to complete it (e.g., as part of your code editor)? I mean, why make a different language, in what situation it could be useful for?  
> **username_3**: The link is dead  
> **username_1**: @PyRulez fixed the link (and added the title of the paper, to help with future breakage).  

---

