Méretkódolt típusokat az algebrai adattípusokból kaphatjuk meg oly módin, hogy az adatkonstruktort kibővítjük az elemek méretével. A legegyszerűbb ilyen típus az lista, amelynek klasszikusan két adatkonstruktora van: az üres lista (Nil) és a listába beszúrás (Cons), ez utóbbi egy elemből és egy listából készít egy új listát, amely elején található az új elem. Ha ezt a típust mérettel bővítjük akkor azt kapjuk, hogy az üres lista mérete 0, a Cons pedig a paraméterül kapott lista méreténél egyel nagyobbat hoz létre. Formálisan:

\(Cons::T->L_{n}(T)->L_{n+1}(T)\)

Amikor függvények típusát adjuk meg méretkódolt típusokkal, az egyszerű esetekben nagyon látványos eredményeket lehet elérni, ilyen például a lista megfordítása, amely a paraméterül kapott listával megegyező elemszámú listával tér vissza. Ilyenkor az okozza a nehézségeket, hogy ez az állítás semmit nem mond arról, hogy ha a lista elemei is listák, mi történik azoknak a méreteivel. Erre a klasszikus megoldás az altípusosság bevezetése, azaz azt mondjuk, hogy egy \(n\) elemű lista altípusa az \(n+1\) eleműnek. Ezáltal a listák listáját úgy kezelhetjük, hogy a legnagyobb elemszámú listát vesszük adjuk meg a lista elemtípusának: \(L_{n}(L_{m}(T))\), ahol a külső lista elemszáma legfeljebb \(n\), a belső lista elemszámának felső korlátja pedig \(m\). Sajnos ez a kézenfekvő megoldással a gyakorlatban előforduló függvények típusaiban szereplő méretekre csak elnagyol felső korlátot tud adni.

Más módszerek lehetnek pontosabbak, ezek általában valami szúk függvényosztályon belül képesek csak a méretkorlátok megállapítására (ilyen jellemző függvényosztály például a monoton vagy a lineáris függvények). Az általam adott megoldásban azonban a függvények tetszőleges polinomok lehetnek.

Munkámban \cite{lncs13,tfp2011,2012-Gobi-LanguageHigherorder} egy olyan kalkulust dolgoztam ki, amely lehetővé teszi azt, hogy a listában található listák elemszámát kifejezzük, így az altípusosság elhagyható, mégis a méretkódolt típusok tetszőleges mélységben egymásba ágyazhatóak. A megoldás lényege, hogy méretek kifejezésében lambda kalkulust használok, amely lehetővé teszi, hogy az indexek függvényében kifejezzük az elemszámot. A cikkben adok egy módszert arra, hogy egy ily módon típusozott függvényből egy SMT (Satisfiability Module Theory) problémát állítottam elő.

A probléma egy másik lehetséges megközelítése a függvények absztrakt interpretációja, amelyet szintén megvizsgáltam. A \cite{fopara_2011} cikkben a függvények absztrakt intepretációját vizsgálom intervallum aritmetikával, ezáltal az adatok méretére adok alsó és felső korlátot egy tisztán funkcionális nyelvre.