A gyakorlatban nagyon fontos szerepet játszik egy speciális rekordtípus. Legyen egy tetszőleges (megszámlálható) halmaz, amelyen van egy rákövetkezési reláció. Jelöljük ezt a rákövetkezési relációt -cal, és inverzére vezessük be a jelölést.

A függvénytípusra is bevezetünk néhány fontos specifikációs függvényt. A továbbiakban legyen . Ekkor

A sorozathoz hasonlóan a függvénytípusra is bevezetünk egy szelekciós parciális függvényt. TekintsÜk a fentiekben használt -et. Ekkor , , és ha , , akkor:

A függvénytípus szelektorfüggvényét nem szoktuk külön elnevezni, helyette a matematikában – a függvény helyettesítési értékének jelölésére – használt zárójeles hivatkozást használjuk, azaz

A függvénytípus elnevezés azt a szemléletes képet tükrözi, hogy egy függvénytípusú érték felfogható egy típusú parciális függvénynek, amelynek értelmezési tartománya a " -tól a -ig tart", és értékeit pedig a sorozat komponens tartalmazza.

Az előbbiekben bevezetett függvényeket kiterjeszthetjük az egész állapottérre is: komponáljuk a megfelelő változóval. Tehát ha például egy sorozattípusú változó, akkor egy az egész állapottéren értelmezett függvény. Az ilyenfajta függvénykompozíciókra bevezetünk egy újabb jelölést: ha a fenti függvények valamelyike, és a neki megfelelő típusú változó, akkor az helyett -t írunk.