Tüübituletus lihtsalt tüübitud {$\lambda$}-arvutuses
Tüüpideks on meil tüübimuutujad ja funktsioonid : {$$ \begin{array}{lcl@{\hspace{5em}}l} \tau & ::= & \alpha & \text{tüübimuutuja} \\ & \mid & \tau_1 \to \tau_2 & \text{funktsioonitüüp} \end{array} $$}
Lihtsalt tüübitud {$\lambda$}-arvutuses (ehk {$\lambda\!\!\rightarrow$}) on kaks standardset süntaksi stiili:
- Church’i-stiil ({$e ::= x\mid e_1\,e_2\mid\lambda x:\tau.\,e$}), milles termid sisaldavad piisavalt tüübiannotatsioone nii et tüübikontroll ja tüübituletus on lihtsad.
- Curry-stiil ({$e ::= x\mid e_1\,e_2\mid\lambda x.\,e$}), milles on termid ilma tüübiannotatsioonideta ja printsipiaalne tüüp on arvutatav polünomiaalse ajaga.
Üldjuhul on Curry-stiilis tüübisüsteemides tüübituletus ja tüübikontroll lahendamatud ülesanded. Nt. teist-järku {$\lambda$}-arvutuse (ehk {$\lambda 2$}) puhul.
Lihtsamate süsteemide jaoks on tüübituletus võimalik. Nt. Hindley-Milner'i polümorfism (ehk HM) puhul.
Tüübituletus {$\lambda\!\!\rightarrow$} a’la Curry jaoks
Tüübituletuse algoritm:
1. Annoteerida iga alamavaldis ja muutuja siduvesinemine unikaalse tüübimuutujaga.
2. Genereeri kitsenduste süsteem kasutades järgnevaid reegleid:
{$$ \color{blue}{ \frac{x^a \in \Gamma}{\Gamma \vdash x^\beta \color{green}{\Rightarrow \{ \alpha = \beta \}}}\textsf{var} \qquad \qquad \frac{\Gamma, x^a \vdash e^\beta \color{green}{\Rightarrow E}}{\Gamma \vdash (\lambda x^\alpha.e^\beta)^\gamma \color{green}{\Rightarrow \{\gamma = \alpha \rightarrow \beta \} \cup E }}\textsf{abs} } $$}
{$$ \color{blue}{ \frac{\Gamma \vdash e^\alpha_1 \color{green}{\Rightarrow E_1} \qquad \qquad \Gamma \vdash e^\beta_2 \color{green}{\Rightarrow E_2}}{\Gamma \vdash ( e^\alpha_1 e^\beta_2)^\gamma \color{green}{\Rightarrow \{\alpha = \beta \rightarrow \gamma \} \cup E_1 \cup E_2 }} \textsf{app}} $$}
3. Lahenda kitsenduste süsteem leides selle kõige üldisema unifitseerija. Kui seda ei leidu, ei ole term järelikult tüübitav.
Kõige üldisema unifitseerija leidmine
Võrrandeid saab lahendada lihtsustusreeglite korduva rakendamise kaudu.
Kaks peamist reeglit:
- Asenda võrdus kujul {$\tau_1\to\tau_2=\tau_3\to\tau_4$} kahe võrdusega {$\tau_1=\tau_3$} ja {$\tau_2=\tau_4$}.
- Olgu võrdus kujul {$\alpha=\tau$}. Kui {$\alpha \in \text{fv}(\tau)$} siis raporteeri viga, vastasel korral asenda kõigis võrdustes {$\alpha$} asemel {$\tau$}.
Abireeglid:
- eemalda reeglid kujul {$\alpha=\alpha$},{$\text{Bool}=\text{Bool}$}, jne.;
- asenda {$\tau=\alpha$} võrdusega {$\alpha=\tau$};
- kui leidub võrdus {$\tau_1=\tau_2$}, kus peatüübikonstruktorid on erinevad (näit. {$\text{Bool}=a_1\to a_2$}), siis raprorteeri viga.