System F

Ten artykuł od 2011-07 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła, najlepiej w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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 ${\displaystyle \sigma }$ oraz ${\displaystyle \tau }$ należą do U, to ${\displaystyle \sigma \to \tau }$ również należy do U,
• jeśli ${\displaystyle \alpha }$ jest zmienną (należy do V) oraz ${\displaystyle \sigma }$ należy do U, to ${\displaystyle \forall \alpha .\ \sigma }$ również należy do U.

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