Jaka jest rola dwukolorowego rachunku konstrukcji?

Czytam więc trochę o opracowaniu, w szczególności algorytmach opartych na dwukolorowym rachunku budowy i jestem trochę zdezorientowany. Nie rozumiem, jaki dokładnie jest cel tego$CC^{bi}$jest. Wydaje się być identyczny z$CC$z wyjątkiem tego, że istnieje rozróżnienie między niejawnymi i jawnymi argumentami funkcji. W szczególności nie widzę, jak pozwala ci pisać$(id\; 0)$ zamiast $(id\; \mathbb{N}\; 0)$. Jeśli przyjmiemy system globalnych definicji, wówczas

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

i

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

Czy reguły naprawdę na to pozwalają $(id\; 0)$? Oczywiście, że tak, ale nie widzę tego w relacji pisania. Czy coś brakuje? Czy rozumiem rolę$CC^{bi}$ nieprawidłowo?

Ponadto, czy nie utracono własności zbiegu? Wydaje mi się, że moim problemem jest to, że czytam o opracowaniu bez większego przeczytania$CC^{bi}$przed tym. Jaki jest dobry artykuł, który go wprowadza i tylko on?

Edycja: Aby być bardziej szczegółowym, pytam jak$(id\; 0)$ jest akceptowane zamiast $(id\; \mathbb{N}\; 0)$ kiedy reguły są zarówno jawne, jak i niejawne $\Pi$aplikacje są identyczne modulo sytnax. Nie widzę żadnej różnicy między$:$ i $|$ zasady dla obu wydają się takie same.

Edycja: Nie mówię o Implicit Calculus of Constructions, która jest inną teorią i ma różne reguły jawnego$\Pi$(aplikacja vs. generacja).

Edycja: OK, chyba zaczynam to rozumieć, ale nie odpowiem na to pytanie, dopóki nie będę pewien. Gruntownie$(id\; 0)$ nie pisze sprawdzania, a tak naprawdę jest tylko rozwinięty $(id\; \mathbb{N}\; 0)$tuż przed sprawdzaniem typu lub wykonywane jako dodatkowa odpowiedzialność algorytmu sprawdzania typu. Zasadniczo te ukryte rachunki mają być językami interfejsu (użytkownika), które są opracowywane w zwykłych (jawnych) rachunkach lub przynajmniej jawnym fragmencie ukrytych rachunków przed sprawdzeniem typu. Jeśli tak jest, to myślę, że widzę duży obraz. Czy ktoś może to potwierdzić?

W Domniemana rachunku konstrukcji rozszerzającej Czysta systemów typu ze skrzyżowania rodzaj spoiwa i Subtyping Alexandre Miquel wprowadza podstawowe pojęcia dotyczące niejawnego rachunku konstrukcji, która moim zdaniem jest synonimem bicolored rachunku konstrukcji.

Chodzi o to, aby (między innymi) mieć rachunek bez bałaganu jawnych adnotacji typu wszędzie. Wnioskowanie typu jest jednak (bardzo prawdopodobne) nierozstrzygalne.

W tym rachunku, jeśli weźmiemy $id=\lambda x. x$, to możesz wyprowadzić

$$\vdash id\colon \forall X\colon Type. X\rightarrow X$$ po prostu używając kolejno produktu jawnego i ukrytych reguł produktu. Wtedy reguła tworzenia instancji dla produktu niejawnego pozwala $$\vdash id\colon Nat\rightarrow Nat$$ a więc $$\vdash id\ 0 \colon Nat$$ System dopuszcza redukcję i konfluencję osobników, nawet na nietypowych warunkach (co w rzeczywistości nie działa w przypadku rachunków z adnotacjami abstrakcyjnymi). Wszystko to można znaleźć w pracy Aleksandra, która niestety jest po francusku. Obawiam się, że nie jestem pewien, czy mam lepsze odniesienie do tych wyników.