System F

Szablon:Dopracować Szablon:Inne znaczenia System F – jeden z wariantów rachunku lambda z typami. Jest to najprostszy rachunek zawierający typy proste oraz typy polimorficzne.

Zbiór typów można zdefiniować jako najmniejszy taki zbiór U, że przy danym, ustalonym i przeliczalnym zbiorze zmiennych V, zachodzą następujące własności:

• V zawiera się w U,
• jeśli $\sigma$ oraz $\tau$ należą do U, to $\sigma \to \tau$ również należy do U,
• jeśli $\alpha$ jest zmienną (należy do V) oraz $\sigma$ należy do U, to $\mathrm{\forall }\alpha .\sigma$ również należy do U.

Typy postaci $\mathrm{\forall }\alpha .\sigma$ należy traktować (nieformalnie) jako każdą możliwą instancję typu $\sigma$ taką, że za każde wystąpienie zmiennej $\alpha$ wstawiamy dowolny inny typ (za każde wystąpienie zmiennej ten sam).