Jak czytać zasady pisania?

Zacząłem czytać coraz więcej prac naukowych dotyczących języków. Uważam to za bardzo interesujące i dobry sposób, aby dowiedzieć się więcej o programowaniu w ogóle. Zazwyczaj jednak pojawia się sekcja, z którą zawsze się zmagam (na przykład część trzecia tego ), ponieważ brakuje mi teoretycznego zaplecza informatycznego: Typ reguł.

Czy są dostępne jakieś dobre książki lub zasoby online, aby zacząć w tej dziedzinie? Wikipedia jest niesamowicie niejasna i tak naprawdę nie pomaga początkującym.

W większości systemów typów reguły typów współpracują ze sobą w celu zdefiniowania ocen formy:

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

Oznacza to, że w kontekście wyrażenie e ma typ τ . Γ jest odwzorowaniem wolnych zmiennych e na ich typy.$\Gamma$$e$$\tau$
$\Gamma$$e$

System typów będzie się składał z zestawu aksjomatów i reguł (formalny system reguł wnioskowania , jak podkreśla Raphael).

Aksjomat ma postać

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

Stwierdza on, że wyrok Uznaje (zawsze).$\Gamma \vdash e:\tau$

Przykładem jest

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

który stwierdza, że ​​przy założeniu, że typem zmiennej jest τ , wówczas wyrażenie x ma typ τ .$x$$\tau$$x$$\tau$

Reguły wnioskowania pobierają ustalone wcześniej fakty i budują z nich większe fakty. Na przykład reguła wnioskowania

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

mówi, że jeśli mam wyprowadzenie faktu i wyprowadzenie z faktu Tt ⊢ e 2 : τ , to mogę otrzymać wyprowadzenie faktu Tt ⊢ e 1 e 2 : τ ' . W takim przypadku jest to reguła dla aplikacji funkcji pisania na klawiaturze.$\Gamma\vdash e_1:\tau\to\tau'$$\Gamma\vdash e_2:\tau$$\Gamma\vdash e_1\ e_2:\tau'$

Istnieją dwa sposoby czytania tej zasady:

• z góry na dół - biorąc pod uwagę dwa wyrażenia (funkcję i inne wyrażenie) oraz pewne ograniczenia dotyczące ich typu, możemy skonstruować inne wyrażenie (zastosowanie funkcji do wyrażenia) z danym typem.
• bottom-up - biorąc pod uwagę wyrażenie, które w tym przypadku jest zastosowaniem funkcji do jakiegoś wyrażenia, sposób ten jest wpisywany najpierw poprzez wpisanie dwóch wyrażeń, upewniając się, że ich typy spełniają pewne ograniczenia, a mianowicie, że pierwsze jest typ funkcji, a drugi ma typ argumentu funkcji.

$\Gamma$$\lambda$

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

Reguły wnioskowania są stosowane indukcyjnie w oparciu o składnię wyrażenia uznawanego za drzewo genealogiczne. Na liściach drzewa (u góry) będą znajdować się aksjomaty, a gałęzie zostaną utworzone przez zastosowanie reguł wnioskowania. Na samym dole drzewa znajduje się wyrażenie, które chcesz wpisać.

$\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'}}}$$

• Rodzaje i języki programowania : Benjamin Pierce
• Praktyczne podstawy języków programowania autorstwa Roberta Harpera

Obie książki są bardzo obszerne, ale zaczynają się powoli, tworząc solidny fundament.

Jest uroczy interaktywny samouczek online na rachunku sekwencyjnym, który może pomóc w budowaniu intuicji i poczuć, jak działa wnioskowanie: Interaktywny samouczek o rachunku sekwencyjnym

Na tej stronie w Wikipedii zaleca się „ Type Systems, Luca Cardelli, ACM Computing Surveys ”, która jest 2-stronicową ankietą, która pomoże ci zrozumieć, jak czytać regułę. W każdym razie sposób czytania reguły jest doskonale wyjaśniony na tej stronie Wikipedii (lub jeszcze lepiej w ankiecie na 2 stronach). Jednak, aby zrozumieć całość, musisz zrozumieć, co to jest system pisania (złożony z kilku reguł), dla którego artykuł w Wikipedii „ System typów ” jest dobrym początkiem (i masz kilka książek w dziale „Materiały referencyjne ” tego stronę, jeśli chcesz iść dalej).