Hindley - Damas - Milner tyyppijärjestelmä

• Teetkö Haskellia harkkana?
• Tässä pohja modernille tyypinpäättelylle

Hindley - Damas - Milner systeemi

Ts. Lambdakalkyyli, johon on lisätty let ja tyypit

• Monotyypit ovat samoja vain itsensä kanssa
• \(\forall\alpha.\alpha\rightarrow\alpha\) on sama kuin haskellin a -> a (tai forall a. a->a)

Kysymys

Onko sallittua kirjoittaa: \(\forall\alpha. \alpha \rightarrow \forall\beta.\beta\)?

\(\Gamma\) - Konteksti

• Huom: Tässä vaiheessa tyypeillä ja lausekkeilla ei ole mitään yhteyttä!
• Raa'asti: Mitä tarkoittaisi tyyppi \(\text{int}\)?
• Tyyppejä voi tarkastella vain kontekstissaan. Merkitys syntyy siinä.

\(\Gamma\) - Konteksti

• "\(x\) on tyyppiä \(\tau\)" merkitään \(x : \tau\)
• \(\Gamma\) on joukko tälläisiä merkintöjä
• Ts. \(\Gamma\) merkitsee jo tiedettyjä tyypityksiä.
• "\(\Gamma,x:\tau\)" tarkoittaa "lisätään kontekstiin tieto, että \(x\) on tyyppiä \(\tau\)"
• "\(\Gamma\vdash x:\alpha\)" tarkoittaa, että annetusta ympäristöstä \(\Gamma\) voidaan päätellä, että \(x\) on tyyppiä \(\alpha\)

Tyypityssäännöt (A)

\[\begin{array}{cl} \displaystyle\frac{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma}&[\text{Var}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\tau \rightarrow \tau' \quad\quad \Gamma \vdash e_1 : \tau } {\Gamma \vdash \text{ap}[e_0;e_1] : \tau'}&[\text{App}]\\ \\ \displaystyle\frac{\Gamma,\;x:\tau\vdash e:\ \color{red}\tau'} {\Gamma \vdash \text{lam}[x; x.e] : \tau \rightarrow {\tau'}}&[\text{Abs}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\color{red}\sigma \quad\quad \Gamma,\,x:\color{red}{\sigma} \vdash e_1:\tau} {\Gamma \vdash \text{let}[x;e_0;x.e_1] : \tau} &[\text{Let}]\\ \\ \\ \end{array}\]

Kääntyvät melko suoraan koodiksi. Huomaa monotyyppi lambdassa ja polytyyppi letissä

Esimerkki

Näytetään, että \(\Gamma \vdash (\lambda x.x+(x+2))\ 5\ : \text{int}\), olettaen, että

1. Tässä tietysti konteksissa on \(5:\text{int}\) ja
2. ja sääntöihin lisätään \(\frac{\Gamma\vdash x:\text{int}\quad \Gamma\vdash y:\text{int}}{\Gamma \vdash x+y:\text{int}}\)

Eli näin:

\[\displaystyle \def\int{\text{int}} \def\fin#1{\frac{}{\displaystyle#1}} \frac{\fin{\Gamma \vdash 5 : \int} \quad \frac{\displaystyle \fin{\Gamma,x:\int\vdash x:\int}\quad\frac{\fin{\Gamma,x:\int\vdash x:\int}\quad\fin{\Gamma\vdash 2:\int}}{\displaystyle \Gamma,x:\int\ \vdash x+2:\int}[\text{plus}]}{\displaystyle\Gamma,x:\int\ \vdash x+(x+2):\int}[\text{plus}]} {\Gamma \vdash (\lambda x.x+(x+2))\ 5\ : \int} [\text{lam}]\]

Esimerkki 2

• Näytetään, että \(\text{let}\ \text{id} = \lambda x . x\ \text{in}\ \text{id} : \forall\alpha.\alpha\rightarrow\alpha\).
• (Ajattele top-level bindejä)

\[\frac{\displaystyle\frac{???}{\Gamma\vdash \lambda x.x:\forall\alpha.\alpha\rightarrow\alpha}[hmm?]\quad \fin{\Gamma,id:\forall\alpha.\alpha\rightarrow\alpha\vdash \text{id}:\forall\alpha.\alpha\rightarrow\alpha}} {\text{let}\ \text{id} = \lambda x . x\ \text{in}\ \text{id} : \forall\alpha.\alpha\rightarrow\alpha}[let]\]

• "hmm?" ei ole Abs-sääntö: \[ \frac{\Gamma,\;x:\tau\vdash e:\ \tau'} {\Gamma \vdash \text{lam}[x; x.e] : \tau \rightarrow {\tau'}}[\text{Abs}]\]

• Tarvitaan lisää sääntöjä:

Tyypityssäännöt (B)

\[\begin{array}{cl} \displaystyle\frac{\Gamma \vdash e:\sigma' \quad \sigma' \sqsubseteq \sigma}{\Gamma \vdash e:\sigma}&[\mathtt{Inst}]\\ \\ \displaystyle\frac{\Gamma \vdash e:\sigma \quad \alpha \notin \text{free}(\Gamma)}{\Gamma \vdash e:\forall\alpha\ .\ \sigma}&[\mathtt{Gen}]\\ \\ \end{array}\]

Vapaat muuttujat (\(\text{free}(\Gamma)\))

• Vapaa muuttuja on olennainen ja helppo käsite
• \(\forall \alpha . \alpha -> \beta\): Tässä \(\beta\) on vapaa.
• \(\forall \beta .(\forall \alpha . \alpha \rightarrow \beta)\): Tässä ei ole vapaita muuttujia.
• \(\text{int} \rightarrow \text{bool}\): Tässä \(\text{Int}\) ja \(\text{Bool}\) ovat vapaita. (Mutta varmaan sidottuja jossain ulomassa lausekkeessa)
• Samoin ympäristölle: jos \(x:\alpha \in\Gamma\), niin \(\alpha\) ei ole vapaa

Vapaat muuttujat (\(\text{free}(\Gamma)\))

• Vapaa muuttuja on olennainen ja helppo käsite
• \(\forall \alpha . \alpha -> \beta\): Tässä \(\beta\) on vapaa.
• \(\forall \beta .(\forall \alpha . \alpha \rightarrow \beta)\): Tässä ei ole vapaita muuttujia.
• \(\text{int} \rightarrow \text{bool}\): Tässä \(\text{Int}\) ja \(\text{Bool}\) ovat vapaita. (Mutta varmaan sidottuja jossain ulomassa lausekkeessa)
• Samoin ympäristölle: jos \(x:\alpha \in\Gamma\), niin \(\alpha\) ei ole vapaa

Vapaiden muuttujien löytäminen

\(\text{Free}(\alpha) = \left\{ \alpha \right\}\)

\(\text{Free}(\text{tap}[D;\tau_1; \dots; \tau_n]) = \bigcup^{n}_{i=0} \text{Free}(\tau_i)\)

\(\text{Free}(\text{forall}[\alpha;\alpha.\sigma]) = \text{Free}(\sigma) \setminus \left\{\alpha\right\}\)

(Kääntyy btw. lähes sanasta sanaan koodiksi)

Erikoistuminen (\(\sqsubseteq\))

• Ajatus lienee, että funktio \(\forall\alpha.\text{list}\ \alpha \rightarrow \alpha\) on käytettävissä myös muodossa \(\text{list}\ \text{int} \rightarrow \text{int}\).
• Tätä merkitään symbolilla "\(\sqsubseteq\)":
  • Esim. \(\forall\alpha.\text{list}\ \alpha \rightarrow \alpha \sqsubseteq \text{list}\ \text{int} \rightarrow \text{int}\)
• Onko esim.
  • \(\forall\alpha.\alpha \sqsubseteq \text{int}\) ?
  • \(\text{int}\sqsubseteq \forall\alpha.\alpha\) ?
  • \(\forall\alpha.\alpha \sqsubseteq \forall\beta.\beta\)?
• Milloin \(\alpha \sqsubseteq \beta\)?

Erikoistuminen

1. \(\displaystyle\frac{\tau'=[\tau/\alpha]\sigma} {\forall\alpha.\sigma \sqsubseteq \tau'}\)

2. \(\displaystyle\frac{\sigma\sqsubseteq\sigma'} {\forall\alpha.\sigma \sqsubseteq \forall\alpha.\sigma'}\)

3. \(\displaystyle\frac{\beta\notin\text{free}(\sigma)} {\forall\alpha.\sigma \sqsubseteq \forall\beta.[\beta/\alpha]\sigma}\)

1. Jos \(\tau'\) on saatu korvaamalla polytyypissä \(\sigma\) sidottu tyyppimuuttuja \(\alpha\) monotyypillä \(\tau\), niin \(\tau'\) on polytyypin \(\sigma\) erikoistuma.

2. Jos \(\forall\):n sisällä on erikoistettu, niin sekin on erikoistuma

3. Sidotut muuttujat saa nimetä uudestaan

Tyypityssäännöt (B)

\[\begin{array}{cl} \displaystyle\frac{\Gamma \vdash e:\sigma' \quad \sigma' \sqsubseteq \sigma}{\Gamma \vdash e:\sigma}&[\mathtt{Inst}]\\ \\ \displaystyle\frac{\Gamma \vdash e:\sigma \quad \alpha \notin \text{free}(\Gamma)}{\Gamma \vdash e:\forall\alpha\ .\ \sigma}&[\mathtt{Gen}]\\ \\ \end{array}\]

Esimerkki 2, yritys 2

• Näytetään, että \(\text{let}\ \text{id} = \lambda x . x\ \text{in}\ \text{id} : \forall\alpha.\alpha\rightarrow\alpha\).
• (Ajattele top-level bindejä)

\[\frac{\displaystyle\frac{\displaystyle\frac{\fin{\Gamma,x:\alpha\vdash x:\alpha}}{\Gamma\vdash\lambda x.x:\alpha\rightarrow\alpha}[Abs]\quad\frac{\Gamma=\emptyset}{\alpha\notin\text{free}(\Gamma)}}{\Gamma\vdash \lambda x.x:\forall\alpha.\alpha\rightarrow\alpha}[Gen]\quad \fin{\Gamma,id:\forall\alpha.\alpha\rightarrow\alpha\vdash \text{id}:\forall\alpha.\alpha\rightarrow\alpha}} {\text{let}\ \text{id} = \lambda x . x\ \text{in}\ \text{id} : \forall\alpha.\alpha\rightarrow\alpha}[let]\]

Havainto

• \(\lambda x.x\) voi yhtä hyvin olla \(\text{bool}\rightarrow\text{bool}\) tai \(\text{int}\rightarrow\text{int}\) tai \(\forall\alpha.\alpha\rightarrow\alpha\)
• Jos tehdään algoritmi, tämä täytyy päättää.
• K: Mikä valitaan?

Havainto

• V: \(\forall\alpha.\alpha\rightarrow\alpha\) tuntuu parhaalle
• Perustelu
  • Huomataan, että relaatio \(\sqsubseteq\) on osittaisjärjestys (transitiivinen, reflexiivinen ja antisymmetrinen)
  • Myöskin, \(\forall\alpha.\alpha\rightarrow\alpha \sqsubseteq \text{int}\rightarrow\text{int}\), mutta jos \(x \sqsubseteq\forall\alpha.\alpha\rightarrow\alpha\) niin \(x \approx \forall\alpha.\alpha\rightarrow\alpha\)
  • Ts. \(\forall\alpha.\alpha\rightarrow\alpha\) on maksimaalinen yleistys/minimaalinen erikoistus termille \(\lambda x.x\)
• Näitä kutsutaan nimellä principal type ja tyypinpäättelyn pitäisi tuottaa mieluiten tälläinen.

Sitten toteutetaan

• Ideat:
  • Käytetään [Gen] sääntöä Let muuttujan sidonnoissa
  • Käytetään [Inst] sääntöä muuttujan tyypityksessä
  • Tehdään kaksi kierrosta AST:n yli: Kerätään rajoitteet, (ratkaistaan) ja kirjataan syntyneet tyypit paikoilleen