Ebben a fejezetben bemutatom, hogy az \ref{calculus}. tézis hogyan alkalmazható a Haskell nyelvben. Ehhez elkészítettem egy funkcionális nyelv és a tézisben definiált kalkulus beágyazását a Haskell nyelvbe, valamint készítettem két interpretert a nyelvhez \cite{studia14}. Az egyik interpreter feladata az, hogy a függvényt és a rajta lévő méretkódolt típusokat összevesse, és elkészítse a megfelelő ”verification condition” halmazt.

A másik elkészített interpreter a beágyazott függvényt Haskellre fordítja. A beágyazás sekély, így a kódot futtató interpreter fordítási időben készít Haskell kódot, oly módon, hogy az ne jelentsen számottevő futási időjű többletköltséget a Haskellben megírt azonos kódhoz képest.