Как читать правила набора текста?

Я начал читать все больше и больше статей по языковым исследованиям. Я нахожу это очень интересным и хорошим способом узнать больше о программировании в целом. Тем не менее, как правило , приходит раздел , где я всегда борюсь с (Возьмем, например , части третьей этой ) , так как мне не хватает теоретической подготовки в области компьютерных наук: Тип правил.

Есть ли хорошие книги или онлайн-ресурсы для начала работы в этой области? Википедия невероятно расплывчата и не очень помогает новичку.

В большинстве систем типов правила типов работают вместе, чтобы определить суждения о форме:

$$\Gamma\vdash e:\tau$$

Это говорит о том, что в контексте выражение e имеет тип τ . Г - отображение свободных переменных е в их типы.$\Gamma$$e$$\tau$
$\Gamma$$e$

Система типов будет состоять из набора аксиом и правил (формальная система правил вывода , как указывает Рафаэль).

Аксиома имеет форму

$$\dfrac{}{\Gamma \vdash e:\tau}$$

Это говорит о том, что суждение выполняется (всегда).$\Gamma \vdash e:\tau$

Примером является

$$\dfrac{}{x:\tau\vdash x:\tau}$$

который утверждает, что в предположении, что тип переменной равен τ , то выражение x имеет тип τ .$x$$\tau$$x$$\tau$

Правила вывода берут факты, которые уже были определены, и строят из них более крупные факты. Например, правило вывода

$$\dfrac{\Gamma\vdash e_1:\tau\to\tau' \quad \Gamma\vdash e_2:\tau}{\Gamma\vdash e_1\ e_2:\tau'}$$

говорит, что если у меня есть вывод факта и вывод факта Γ ⊢ e 2 : τ , то я могу получить вывод факта Γ ⊢ e 1 e 2 : τ ′ , В данном случае это правило для набора функций приложения.$\Gamma\vdash e_1:\tau\to\tau'$$\Gamma\vdash e_2:\tau$$\Gamma\vdash e_1\ e_2:\tau'$

Есть два способа прочтения этого правила:

• сверху вниз - учитывая два выражения (функция и другое выражение) и некоторые ограничения на их тип, мы можем создать другое выражение (применение функции к выражению) с данным типом.
• снизу вверх - с учетом выражения, которое, в данном случае, является применением функции к какому-либо выражению, способ, которым это типизируется, заключается в том, чтобы сначала ввести два выражения, гарантируя, что их типы удовлетворяют некоторым ограничениям, а именно то, что первое является тип функции и что второй имеет тип аргумента функции.

$\Gamma$$\lambda$

$$\dfrac{\Gamma x:\tau\vdash e:\tau'}{\Gamma\vdash \lambda x.e:\tau\to \tau'}$$

Правила вывода применяются индуктивно на основе синтаксиса рассматриваемого выражения для формирования деривационного дерева. На листьях дерева (вверху) будут аксиомы, а ветви будут формироваться путем применения правил вывода. В самом низу дерева находится выражение, которое вы хотите набрать.

$\lambda f.\lambda x.f\ x$

$$\dfrac{\dfrac{}{f:\tau\to\tau',x:\tau\vdash f:\tau\to\tau'} \qquad \dfrac{}{f:\tau\to\tau',x:\tau\vdash x:\tau}} {\dfrac{f:\tau\to\tau',x:\tau\vdash f\ x:\tau'}{ \dfrac{f:\tau\to\tau'\vdash \lambda x.f\ x:\tau'}{\vdash \lambda f.\lambda x.f\ x:\tau'}}}$$

• Типы и языки программирования Бенджамина Пирса
• Практические основы языков программирования Роберта Харпера

Обе книги очень всеобъемлющие, но они начинаются медленно, закладывая прочную основу.

Существует мило интерактивный онлайн учебник по секвенции исчисления, которые могут помочь построить некоторые интуитивные и почувствовать , как логический вывод работы: Интерактивное учебное пособие по секвенции Исчисление

На этой странице Википедии рекомендуется " Системы типов, Лука Карделли, ACM Computing Surveys ", это двухстраничный опрос, который может помочь вам понять, как читать правила. Во всяком случае, как прочитать правило прекрасно объясняется на этой странице Википедии (или даже лучше в опросе на 2 страницы). Однако, чтобы понять все это, вам нужно понять, что такое система ввода (составленная из нескольких правил), для которой статья в Википедии " Система типов " является хорошим началом (и у вас есть несколько книг в разделе " Ссылки " этого страница, если вы хотите пойти дальше).