System F

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj
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 oraz należą do U, to również należy do U,
  • jeśli jest zmienną (należy do V) oraz należy do U, to również należy do U.

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