System F

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj
Ujednoznacznienie Ten artykuł dotyczy wariantu rachunku lambda. Zobacz też: Ferry Corsten.

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 \forall\alpha.\ \sigma również należy do U.

Typy postaci \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).