Uniwersytet Warszawski University of Warsaw
Menu
Wyszukiwarka
 W bieżącym katalogu
next up previous
Next: Unifikacja Up: Autoreferat pracy doktorskiej pt. Previous: Zastosowania rachunku

Wyprowadzanie typów

W zwi±zku z powy¿szymi zastosowaniami pojawiaj± siê w literaturze problemy decyzyjne dotycz±ce os±dów wyprowadzalnych w powy¿szych rachunkach. W ogólno¶ci typowy os±d rachunku $\lambda$ z typami ma postaæ

\begin{displaymath} \Gamma\motyka M : \tau, \end{displaymath}

gdzie $\Gamma$ jest otoczeniem zawieraj±cym informacje o obiektach, których deklaracje znajduj± siê poza termem $M$, a $\tau$ jest typem termu $M$. Problemy decyzyjne dla takich os±dów polegaj± na znalezieniu algorytmu, który dla danego niepe³nego os±du potrafi go uzupe³niæ, tak ¿eby wynik da³ siê wyprowadziæ w interesuj±cym nas rachunku. Problem wyprowadzania typów, który nas tutaj interesuje ma jako dane term $M$ i chodzi w nim o znalezienie kontekstu $\Gamma$ oraz typu $\tau$, które pozwol± na wyprowadzenie os±du $\Gamma\motyka M : \tau$. Rozwa¿aæ tak¿e bêdziemy wariacjê tego problemu zwan± kontekstowym wyprowadzaniem typów, w której danymi s± term $M$ oraz kontekst $\Gamma$, a chodzi o znalezienie typu $\tau$, który pozwoli na wyprowadzenie powsta³ego os±du.

Pierwszy z tych problemów ma zastosowanie w sytuacji, gdy próbujemy w jêzyku funkcyjnym napisaæ modu³, który bêdzie mo¿na u¿ywaæ w ró¿nych projektach programistycznych bez konieczno¶ci ponownej jego kompilacji. Musimy dla takiego modu³u okre¶liæ, jakich zewnêtrznych komponetnów potrzebuje on do dzia³ania oraz jakie daje wyniki. Korzystaj±c z algorytmu wyprowadzania typów, dowiadujemy siê z otrzymanego kontekstu $\Gamma$, jakie s± wymagania dotycz±ce zewnêtrznych komponentów dla danego elementu modu³u, za¶ z otrzymanego typu $\tau$, jakie element modu³u daje wyniki.

Drugi z problemów -- kontekstowe wyprowadzanie typów -- znajduje zastosowanie w jêzykach funkcyjnych w sytuacji, gdy po prostu usi³ujemy okre¶liæ, jaki typ ma nasz program (jakiego rodzaju wyniki daje). Mamy tutaj znane otoczenie (kontekst), w którym znajduj± siê typy dla wszystkich u¿ywanych w jêzyku sta³ych oraz dla ju¿ zdefiniowanych operacji, mamy napisany program, którego w³asno¶æ nas interesuje i oczekujemy na automatyczne wyprowadzenie tej w³asno¶ci. Algorytmy rozwi±zuj±ce tego rodzaju problemy s± w tej chwili standardowym elementem systemów jêzyków funkcyjnych wywodz±cych siê od ML-a.

next up previous
Next: Unifikacja Up: Autoreferat pracy doktorskiej pt. Previous: Zastosowania rachunku
Aleksy Schubert 2001-03-15