{refsection}

1. Tézis: Típuskikövetkeztetési algoritmust adtam arra az esetre, amiben a változók típusa a kikövetkeztetett típustól függhet. A megoldás a közismert Bottom–Up típuskikövetkeztető algoritmuson alapszik, ahol a típusegyenletek megoldásának késleltetésével lehetővé tehető a környezetfüggő egyenletek felírása. Az algoritmust az F# nyelv fogalomrendszerén belül definiáltam. afterindentfalseafterheading

A méretek intervallum aritmetikai vizsgálatát az F# nyelv egy tisztán funkcionális résznyelvén is vizsgáltam, azonban az absztrakt interpretációnak előfeltétele volt, hogy tetszőleges részkifejezések típusát ismerjük annak futtatása során. A bonyodalmakat az okozta, hogy az F# nyelvben lévő rekord adattípusok (osztályok) mezőihez a funkcionális nyelvek a rekordok mezőihez elérőfüggvényeket rendelnek, azonban, ha két rekord azonos nevű mezőt tartalmaz, az elérőfüggvények neve is meg fog egyezni, ez viszont a klasszikus Hindley–Milner típusrendszerben nem megengedett, ott a kikövetkeztetés megkezdésekor a szimbólumok típusait egyértelműen ismernünk kell. A helyzetet tovább bonyolították az F# nyelv rendkívül bonyolult láthatósági szabályai, amelyek ráadásul függenek a már kikövetkeztetett típusoktól is.

A megoldás keresésében az első lépcső \cite{icai2010_scope} az volt, hogy a kikövetkeztetést és a névfeloldást szét kellett választani. Ehhez közismert Bottom–Up típuskikövetkeztetési algoritmusnak kihasználtam azt a tulajdonáságát, hogy az algoritmus két menetben dolgozik: első menetben típusegyenleteket ír fel a, a második menetben pedig ezeket megoldja. A második menetben az egyenletek megoldásának sorrendje nem teljesen kötött, így a nem egyértelmű típusok egyenletének a felírását elhalaszthatjuk. Amikor a már megoldható típusegyenletek elfogytak, elindítunk egy névfeloldást, ami a már rendelkezésre álló típusok alapján próbálja a névfeloldást elvégezni, a sikeresen feloldott nevekkel bővítve a típusegyenlet-rendszert. Ily módon a típuskikövetkeztetési és névfeloldási lépések egymás utáni ismétlésével a feladat iteratívan megoldható.

A fenti algoritmus használatával definiáltam \cite{macs2010} az F# nyelv egy tisztán funkcionális G\(\flat\) résznyelvét. Ez a megoldás lehetővé teszi a \ref{calculus} tézis alkalmazását az F# nyelvre.

\printbibliography